« The

SMT Solver »


Page Content:


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


Shostak-like theories combination




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