Why3 (original) (raw)
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. (See the list of supported provers below.) 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. (See Projects using Why3 below.) Why3 can be easily extended with support for new theorem provers. Why3 can be used as a software library, through an OCaml API.
Documentation and Examples
Related Publications
- Logic
- Programming language and Environment
- Applications and Case Studies
- Verifying Two Lines of C with Why3: an Exercise in Program Verification (VSTTE 2012) [bib]
- Discharging Proof Obligations from Atelier B using Multiple Automated Provers [bib]
- Binary heaps formally verified in Why3 [bib]
- Verified programs with binders (PLPV 2014) [bib]
- Let's verify this with Why3 [bib]
Examples, Galleries of Verified Programs
- Visit ourgallery of verified programs, as part of a larger gallery on the website of Toccata.
- A mini-gallery of verified sorting algorithms, by J.-J. Levy and C. Ran
- A gallery of verified programs involving floating-point arithmetic, by S. Boldo
- A mini-gallery of verified logical algorithms, by P. Barroso, A. C. Silva, M. Pereira, A. Ravara and S. M. Sousa ofNOVA-LINCS
Lecture Notes
- Video: Tutorial: Why3 tool for deductive program verification by Sandrine Blazy (Tutorial Series of the FME Teaching Committee)
- Deductive Program Verification with Why3 (lecture at Digicosme Spring School 2013)
- (in French) Vérification déductive de programmes avec Why3 (JFLA, France, 2012)
Other Student Lectures using Why3
(Do not hesitate to contact us if you use Why3 for teaching, we would be happy to add a link to your course's page here)
- (in Portuguese) Course Formal methods for Software Engineering at the Universidade do Minho, Portugal
- Course Proofs of Programs at the Master Parisien de Recherche en Informatique
- (in Portuguese) Courses Formal methods and Certified Programming at the Universidade da Beira Interior, Portugal
- (in French) course Méthodes formelles et développement de logiciels sûrs at the Master Informatique de l'Université de Rennes
- (in French) course Programmation de confiance at the Licence Informatique de l'Université de Rennes
- (in French) course sémantique des langages, third year ofCentraleSupelec Engineering School
- course Bug Catching: Automated Program Verification, Carnegie Mellon University, USA
Projects using Why3
(Contact us if you want your project listed here)
- EasyCrypt: toolset for reasoning about relational properties of probabilistic computations with adversarial code
- Frama-C: extensible and collaborative platform dedicated to source-code analysis of C software; and itsWP plug-in for deductive verification
- SPARK 2014: formal verification tool for Ada. See also the ProofInUse project
- CAPS: A Calculational Assistant for Programming from Specifications
- AstraVer project for deductive verification of Linux kernel code
- Formal Verification for Solidity Contracts
- Formal Combinatorics: Formally specified and verified enumeration programs
- Archetype: a domain-specific language to develop Smart Contracts on the Tezos blockchain, with a specific focus on contract security
- Cameleer: a Deductive Verification Tool for OCaml
- QBricks: open-source environment for automated formal verification of quantum programs
- ParcourSup: verification of ranking algorithms used in the French national system for admission in Universities and superior schools.
- Why3-do: A WhyML library for reasoning about state machine specifications and distributed systems.
- Creusot: A program Verifier for Rust programs. See also Creusot: a foundry for the deductive verication of Rust programs
- Formal analysis of temporal properties of Ladder programs
- CoLiS: a project for verification of Debian packages installation scripts.
Some papers from users of Why3
(Contact us if you would like your paper to be listed here)
- WhylSon: Proving your Michelson Smart Contracts in Why3 Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, Simão Melo de Sousa, also available as A tool for proving Michelson Smart Contracts in Why3
- Provable multicore schedulers with Ipanema: application to work conservation Baptiste Lepers, Redha Gouicem, Damien Carver, Jean-Pierre Lozi, Nicolas Palix, Maria-Virginia Aponte, Willy Zwaenepoel, Julien Sopena, Julia Lawall, Gilles Muller
- Ilinva: Using Abduction to Generate Loop Invariants Mnacho Echenim, Nicolas Peltier, Yanis Sellami
- Formal Verification of Control Systems Properties with Theorem Proving Dejanira Araiza-Illan, Kerstin Eder, Arthur Richards
- Suppl : A Flexible Language for Policies Robert Dockins and Andrew Tolmach
- Verification and testing of mobile robot navigation algorithms: A case study in SPARK Piotr Trojanek and Kerstin Eder
- Automated algebraic analysis of structure-preserving signature schemes by Joeri de Ruiter
- Software product line for semantic specification of block libraries in dataflow languages by A. Dieumegard, A. Toom, M. Pantel.
- Rodin Platform Why3 Plug-In by Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander Romanovsky
- Automated Verification of Functional Correctness of Race-Free GPU Programs by Kensuke Kojima, Akifumi Imanishi1, Atsushi Igarashi
- (in French) Preuve de programmes d'énumération avec Why3 by Alain Giorgetti, Rémi Lazarini
- Thread Scheduling in Multicore Operating Systems by Redha Gouicem
- CISE3: Verifying Weakly Consistent Applications with Why3 by Filipe Meirim, Máario Pereira, and Carla Ferreira
- Architecture of a Machine Code Deductive Verification System by Alexander Kamkin, Alexey Khoroshilov, Artem Kotsynyak, Pavel Putro and Ilya Gladyshev
- An Automated Deductive Verification Framework for Circuit-building Quantum Programs by Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle and Benoît Valiron
- End-to-end translation validation for the halide language by Basile Clément and Albert Cohen
- Verifying Fortran Programs with CIVL by Wenhao Wu, Jan Hückelheim, Paul D. Hovland and Stephen F. Siegel
- Why3-do: The Way of Harmonious Distributed System Proofs by Cláudio Belo Lourenço and Jorge Sousa Pinto
- A Formalization of Core Why3 in Coq by Joshua M. Cohen and Philip Johnson-Freyd
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
why3 config --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, CVC4, and Z3. They are free software, available for many architectures, and all together provide a fairly efficient prover support.
For more advanced use, installing Coq is also good to discharge complex VCs. It is also useful to understand why VCs are not proved, that is to debug the input program or its specification.
Automatic provers
Alt-Ergo
an SMT-based theorem prover supporting quantifiers, polymorphic sorts, and various theories including equality, linear and non-linear arithmetic over integers or rational numbers, arrays, records, enumerated types; available from this page.
Beagle
a theorem prover for first-order logic with equality over linear integer/rational/real arithmetic; available from this page
Colibri and Colibri2
SMT solvers based on ideas of constraint logic programming. Support quantifiers and theories including equality, arithmetic, bitvectors, floating-point numbers; available from this page
CVC4
an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors; available from this page
cvc5
an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors; available from this page
dReal
a solver dedicated to formulas on real arithmetic; available from this page
E prover
a theorem prover for first-order logic with equality; available from this page
Gappa
a solver specialized on the verification of numeric formulas, including floating-point numbers; available from this page
Metis
a theorem prover for first order logic with equality; available from this page
Metitarski
a prover specialized on verification of numeric formulas; available from this page
Princess
a prover for first-order logic modulo linear integer arithmetic; available from this page
Psyche
a modular platform for automated or interactive theorem proving; available from this page
SPASS
a theorem prover for first-order logic with equality; available from this page
Vampire
a theorem prover for first-order logic with equality; available fromthis page
veriT
an SMT-based theorem prover supporting quantifiers, equality, linear arithmetic over integers or rational numbers; available from this page
Yices
an SMT solver supporting equality, linear real and integer arithmetic, bitvectors, scalar types, and tuples; available from this page. Both Yices1 and Yices2 can be used, although Yices2 do not support quantifiers.
Z3
an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors; available fromthis page
Interactive provers, a.k.a. Proof assistants
Coq
a proof assistant in intuitionistic logic based on the calculus of inductive constructions; available from this page
PVS
a specification and verification system; available from this page
Isabelle/HOL
a proof assistant in higher-order logic; available from this page
