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:
- the free theory of equality with uninterpreted symbols,
- linear arithmetic over integers and rationals,
- non-linear arithmetic,
- polymorphic functional arrays,
- enumerated datatypes,
- record datatypes,
- associative and commutative (AC) symbols,
- fixed-size bit-vectors.
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
- BWare (2013 - 2016)
- Cafein (2013 - 2016)
- FUI Hi-Lite (2010 - 2013)
- Decert (2009 - 2012)
- ADT Alt-Ergo (2009 - 2011)
- A3PAT (2005 - 2009)
A Collaborative Framework for Non-Linear Integer Arithmetic Reasoning in Alt-Ergo.
Sylvain Conchon, Mohamed Iguernelala and Alain Mebsout. SYNASC, 2013 (to appear).
A Simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic.
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. IJCAR, 2012. [bib] [download the prototype]
Built-in treatment of an axiomatic floating-point theory for SMT solvers.
Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. SMT, 2012. [bib]
Shostak-like theories combination
Canonized rewriting and ground AC completion modulo Shostak theories: Design and implementation.
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. LMCS, 2012. [bib]
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories.
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. TACAS, 2011. [bib]
CC(X): Semantical combination of congruence closure with solvable theories.
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. ENTCS, 2007. [bib]
CC(X): Efficiently combining equality and solvable theories without canonizers.
Sylvain Conchon, Évelyne Contejean, and Johannes Kanig. SMT Workshop, 2007. [bib]
Reasoning with triggers.
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. SMT workshop, 2012. [bib]
Implementing Polymorphism in SMT solvers.
François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. SMT Workshop, 2008. [bib]
Improving Coq propositional reasoning using a lazy CNF conversion scheme.
Stéphane Lescuyer and Sylvain Conchon. FroCoS, 2009. [bib]
A reflexive formalization of a SAT solver in Coq.
Stéphane Lescuyer and Sylvain Conchon. TPHOLs, 2008. [bib]
Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant.
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. AFM, 2007. [bib]
Strengthening the Heart of an SMT-Solver: Design and Implementation of Efficient Decision Procedures.
Mohamed Iguernelala. PhD thesis, 2013. [bib]
SMT Techniques and their Applications: from Alt-Ergo to Cubicle.
Sylvain Conchon. Habilitation thesis, 2012. [bib]
Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
Stéphane Lescuyer. PhD thesis, 2011. [bib]