Overview
Why3 is the 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.See the specific section below for the list of supported provers.
Why3 is developed in the
team-project ProVal (INRIA
Saclay-Île-de-France / LRI Univ Paris-Sud 11 / CNRS)
Contact
User mailing list
Project page on INRIA GForge
Download
Official releases
Git source repository
Documentation
PDF
manual (version 0.72)
Quick migration guide from Why
2.xx to Why3
Related Publications
Examples
Gallery of verified
programs, as part of a larger gallery on the website
of ProVal.
External Provers
This section gives a few tips to download, install and/or configure
external provers. Each time a new prover is installed, you must rerun
the command why3config --detect. Using the latest version is
recommended (except for Yices, see below) and the config tool above
will tell you if the version detected is supported or not.
People
