Why3 - The Why3 platform
Date of the last release: 04 December 2014
Person in charge :
FILLIÂTRE Jean-Christophe
Why is a software verification platform. It provides a set of tools for deductive verification of Java and C source code. Requirements are
specified as annotations in the source, in a special style of
comments. For Java, these specifications are given
in JML and are interpreted by the Krakatoa tool. For C, we
designed our own specification language, largely inspired from JML.
Those are interpreted by the Caduceus tool.
A back-end tool also called Why serves as the VCG. It differs from other systems in that it outputs conditions for several existing provers: interactives ones (Coq, Isabelle/HOL, PVS, HOL-light, Mizar) and automatic ones (Simplify, Alt-Ergo, and SMT provers Yices, CVC3, Z3, haRVey, etc.).
More information: http://why3.lri.fr/
Software - Licence :
LGPL
Research activities
Members
FILLIÂTRE Jean-Christophe
Group
Joint Inria project team Toccata
