Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Why3
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:

Software - Licence : LGPL

Research activities

  FILLIÂTRE Jean-Christophe


Joint Inria project team
Software & patents

Deep Neural Architectures for DNA