Section: New Software and Platforms

Why3

The Why3 environment for deductive verification

Keywords: Formal methods - Trusted software - Software Verification - Deductive program verification

Functional Description

Why3 is an environment 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.

• Participants: Jean-Christophe Filliatre, Claude Marche, Guillaume Melquiond, Andriy Paskevych, François Bobot, Martin Clochard and Levs Gondelmans

• Partners: CNRS - Université Paris-Sud

• Contact: Claude Marche

• URL: http://why3.lri.fr/