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.

AuthorsFrançois Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond and Andrei Paskevich
LicenseLGPL-2.1-only
Published
Homepagehttp://why3.lri.fr/
Issue Trackerhttps://gitlab.inria.fr/why3/why3/issues
Maintainerguillaume.melquiond@inria.fr
Dependencies
Optional dependencies
Source [http] https://why3.gitlabpages.inria.fr/releases/why3-0.73.tar.gz
sha256=99653cd09a90776b975393ca14bdfc1fb3402b7a98ff40930d4fe3a57e6ce368
md5=8994f147b7fc4084da46e81693e044bb
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/why3/why3.0.73/opam
Optionally used by