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.Supported provers: Alt-Ergo, Z3, CVC3, Yices 1, Simplify, Gappa, Coq
Why3 is developed in the
team-project ProVal (INRIA
Saclay-Île-de-France / LRI Univ Paris-Sud 11 / CNRS)
Download
Official releases
Git source repository
Documentation
PDF
manual (version 0.71)
Quick migration guide from Why
2.xx to Why3
Publications
Examples
Gallery of verified
programs, as part of a larger gallery on the website
of ProVal.
People
Contact
User mailing list
