• en

why3 0.80

Maintainer contact@ocamlpro.com
Dependencies
& alt-ergo
coq 8.3
ocamlgraph 1.8.2
sqlite3-ocaml
Optional dependencies
lablgtk
Published Mar 22, 2013
Source [http] https://gforge.inria.fr/frs/download.php/31724/why3-0.80.tar.gz
4b50adf812a34879be92f27f25be7ec9
Edit https://github.com/ocaml/opam-repository/tree/master/packages/why3/why3.0.80/opam

Next generation of the Why software verification platform

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.

No package is dependent