Alt-Ergo
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.
Technologies
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:
- empty theory
- linear integer arithmetic
- linear rational arithmetic
- non-linear arithmetic
- floating point arithmetic
- polymorphic arrays
- enumerated datatypes
- AC symbols
- record datatypes
Industrial uses
There are several verification platforms built on top of Alt-Ergo:
- Why3, a platform for deductive program verification, uses Alt-Ergo as its main prover;
- CAVEAT, a C-verifier developed by CEA and used by Airbus; Alt-Ergo was included in the qualification DO-178C of one of its aircraft;
- Frama-C, a framework to analyse C-code, uses Alt-Ergo in the Jessie and WP plugins (dedicated to "deductive program verification");
- SPARK, uses Alt-Ergo (behind GNATprove) to automate the verification of some assertions in Spark 2014;
- Atelier-B can use Alt-Ergo instead of its main prover (increasing success from 84% to 98% on the ANR Bware project benchmarks);
- Rodin, a B-method framework developed by Systerel, can use Alt-Ergo as a back-end;
- Cubicle, an open source model checker for verifying safety properties of array-based transition systems.
- EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code.