Français Anglais
Accueil Annuaire Plan du site
Accueil > Production scientifique > Logiciels et brevets
Production scientifique
Logiciel Why3
Why3 - La plateforme Why3
Date de dernière version : 04 décembre 2014

Responsable : FILLIÂTRE Jean-Christophe

Why3 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.).

Pour en savoir plus:

Logiciel - Licence : LGPL

Activités de recherche

  FILLIÂTRE Jean-Christophe


Equipe-projet Inria
Logiciels et brevets
Query Intermediate Representation Library

Database of RNA Recurrent Interaction Networks

Static analyzer for dynamics of Automata Networks