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

Logiciel - Licence : LGPL



Activités de recherche

Membres
  FILLIÂTRE Jean-Christophe

Equipe

Equipe-projet Inria
  Toccata
Logiciels et brevets
TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas

BOLDR
Query Intermediate Representation Library