Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Software & patents
Research results
Software Alt-Ergo
Alt-Ergo - The Alt-Ergo theorem prover
Date of the last release: 01 January 2014

Person in charge : CONCHON Sylvain


Alt-Ergo is a \\\"little engine\\\" of proof dedicated to program verification, whose development started in 2006.

It solves goals that are directly written in the Why\\\'s annotation language; this means that Alt-Ergo fully supports first order polymorphic logic with quantifiers.

It also supports the SMT standard defined by the SMT-lib initiative.

More information: http://alt-ergo.lri.fr/

Software - Licence : CeCILL-C



Research activities
  Automated Proof, SMT and Applications
  Deductive Verification of Programs

Members
  CONTEJEAN Evelyne
  CONCHON Sylvain
  LESCUYER Stéphane
  IGUERNELALA Mohamed
  MEBSOUT Alain

Group
  Verification of Algorithms, Languages and Systems

Joint Inria project team
  Toccata
Software & patents
DNADNA
Deep Neural Networks for DNA

TOUCHTOKENS
Low-cost Solution for Tangible Interfaces

LODATLAS
Browsing Linked Data Catalogs with LODAtlas