Description

Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Published: 21 Nov 2013

Dependencies (5)

  1. sqlite3
  2. alt-ergo
  3. coq = "8.3"
  4. ocamlgraph = "1.8.2"
  5. ocaml < "4.06.0"

Reverse Dependencies

    None

Conflicts

    None
Next generation of the Why software verification platform

Install

Documentation status is unknown. why3.lri.fr Edit opam file

Authors

  1. F
    François Bobot
  2. J
    Jean-Christophe Filliâtre
  3. C
    Claude Marché
  4. G
    Guillaume Melquiond
  5. A
    Andrei Paskevich

Maintainers

  1. G
    guillaume.melquiond@inria.fr

Sources

why3-0.80.tar.gz
md5=4b50adf812a34879be92f27f25be7ec9