• en

why3

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.

Authors François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond and Andrei Paskevich
License GNU Lesser General Public License version 2.1
Homepage http://why3.lri.fr/
Maintainer Francois.Bobot@cea.fr (after 0.80)
Tags deductive, program verification, formal specification, automated theorem prover and interactive theorem prover

Events

May 6, 2014

Published version 0.83

Jan 8, 2014

Published version 0.82

Apr 2, 2013

Published version 0.81

  • Andrei Paskevich gained authorship.
  • Claude Marché gained authorship.
  • François Bobot gained authorship.
  • Guillaume Melquiond gained authorship.
  • Jean-Christophe Filliâtre gained authorship.
  • Now licensed under GNU Lesser General Public License version 2.1.
  • Francois.Bobot@cea.fr assumed maintainership from contact@ocamlpro.com.
  • http://why3.lri.fr/ added as homepage.

Mar 22, 2013

Published version 0.80

Aug 21, 2012

Published version 0.73