Alt-Ergo is an automatic solver for mathematical formulas, specifically designed for program verification. It is based on satisfiability modulo theories (SMT). It is distributed under an open-source license (Cecill-C). Its original authors were Sylvain Conchon and Evelyne Contejean, at LRI, but it is now developed and maintained at OCamlPro.
Contents
Design choices
Contrary to most SMT solvers, Alt-Ergo uses a specific input language with prenex polymorphism. This helps reducing the number of quantified axioms and the complexity of problems. It also partially supports SMT-LIB 2 language, but performs less efficiently on SMT files.
Main components
The core of Alt-Ergo is made of three parts: a DFS-based SAT solver, a quantifiers instantiation engine based on E-Matching, and a combination of decision procedures for a set of built-in theories.
Built-in theories
Alt-Ergo implements (semi-)decision procedures for the following theories:
Industrial uses
There are several verification platforms built on top of Alt-Ergo: