why3
| Maintainer | https://github.com/ocaml/opam-repository/issues | |||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Dependencies |
| |||||||||||||||||||||
| Optional dependencies |
| |||||||||||||||||||||
| Available | ocaml-version < "4.06.0" | |||||||||||||||||||||
| Published | Aug 21, 2012 | |||||||||||||||||||||
| Source [http] | https://gforge.inria.fr/frs/download.php/31257/why3-0.73.tar.gz 8994f147b7fc4084da46e81693e044bb | |||||||||||||||||||||
| Statistics | Not installed in the last month. | |||||||||||||||||||||
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/why3/why3.0.73/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.
