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: http://why3.lri.fr/

Logiciel - Licence : LGPL



Activités de recherche

Membres
  FILLIÂTRE Jean-Christophe

Equipe

Equipe-projet Inria
  Toccata

CODALAB
open source framework for running competitions

DNADNA
Deep Neural Architectures for DNA

CARTOLABE
CARTOLABE