why3version
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.
| Authors | François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond and Andrei Paskevich |
|---|---|
| License | LGPL-2.1-only |
| Published | |
| Homepage | http://why3.lri.fr/ |
| Issue Tracker | https://gitlab.inria.fr/why3/why3/issues |
| Maintainer | guillaume.melquiond@inria.fr |
| Dependencies |
|
| Optional dependencies | |
| Source [http] | https://why3.gitlabpages.inria.fr/releases/why3-0.80.tar.gz sha256=32efd5d95744e7e67d223232a2cb6473d126b50d86c3a18f5971f04df08e6f9b md5=4b50adf812a34879be92f27f25be7ec9 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/why3/why3.0.80/opam |
Optionally used by
- frama-c>=16.0 & <20.0
- frama-c-basebuild & >=13.1
- why=2.34
