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 author was Sylvain Conchon, 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 polymorphism, that helps reduce the number of quantified axioms, and thus, the search space. It can read SMT files, but will perform less efficiently on them.
Builtin Theories
Alt-Ergo implements the following builtin theories:
- empty theory
- linear integer and rational arithmetic
- non-linear 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 their recent aircrafts;
- 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 transtion systems.
- EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code.