« The

SMT Solver »

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:

• 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)

Related Publications

Arithmetic

• 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]

Quantifiers

• 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]

Certification

• 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]

Theses

• 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]