« The

SMT Solver »

 


Page Content:

Overview

Alt-Ergo is an open-source SMT solver dedicated to the proof of mathematical formulas generated in the context of program verification. It is built upon CC(X): a congruence closure algorithm parametrized by a Shostak theory X. Currently, Alt-Ergo provides a built-in support for the following theories:

Alt-Ergo is highly parametrized and modular. Each component is described by a set of inference rules and is implemented as an OCaml (parametrized) module. Its native input language is a polymorphic first-order logic modulo theories. It also provides a partial support for the SMT-LIB (v1.2 and v2) standard inputs. Since September 2013, Alt-Ergo is maintained and distributed by the OCamlPro company, while academic research is conducted in partnership with the VALS/Toccata teams (LRI).


 
 

Research Projects Involving Alt-Ergo

 

Related Publications

Arithmetic

Shostak-like theories combination

Quantifiers

Certification

Theses

 
 
 
 
INRIA Saclay - Île-de-France Université Paris-Sud CNRS LRI