Overview

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.

Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.

See the specific section below for the list of supported provers.

Why3 is developed in the team-project Toccata (formerly ProVal) at INRIA Saclay-Île-de-France / LRI Univ Paris-Sud 11 / CNRS.

Contact

Download

People

Documentation and Examples

Related Publications

Examples

Lecture Notes

Other Student Lectures using Why3

Projects using Why3

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.

For beginners with Why3, we recommend to install Alt-Ergo, CVC3, and Z3. They are open-source, available for many architectures, and together provide a fairly efficient prover support.

For more advanced use, installing Coq is also good to discharge complex VCs, such as when induction is required. It is also useful to understand why VCs are not proved, that is to debug the input program or its specification. In case of using Coq, we recommend to give a try to the why3 Coq tactic.

Automatic provers
Alt-Ergo
available under binary form for Unix and Windows, or under source form to be compiled using the OCaml compiler, from this page.
CVC3
available under source form and as a Linux binary from this page
CVC4
available under source form and as a Linux binary from this page
E-prover
available under source form as well as some binary format from this page
Gappa
a prover specialized on verification of numeric formulas, including floating-point numbers, available under source form from this page
Simplify
available under binary form for various architectures from this page or directly here
SPASS
available under source form as well as some binary format from this page
Vampire
available under binary form from this page
veriT
available under source form from this page
Yices
available under binary form for various platform from this page. (Note that Yices version 2 which participated to the SMT-COMP 2009 has no support for quantifiers; thus you should not use it with Why.)
Z3
available under source form from this page
Interactive provers, a.k.a. Proof assistants
The Coq proof assistant
The PVS specification and verification system

INRIA Saclay - Île-de-France              Université Paris-Sud              CNRS              LRI