Software:Alt-Ergo
 | |
| Developer(s) | OCamlPro |
|---|---|
| Type | Mathematical solver, program verifier |
| Website | https://alt-ergo.ocamlpro.com |
Alt-Ergo, an automatic solver for mathematical formulas, is primarily utilized in program verification. It operates on the principle of satisfiability modulo theories (SMT) and is available under the open-source CeCILL-C license. The development of Alt-Ergo was undertaken by researchers at the Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France, and CNRS. Since 2013, the management and oversight of Alt-Ergo have been conducted by OCamlPro company.[1]
Technologies
Design choices
Alt-Ergo employs a specialized input language with prenex polymorphism, designed to reduce the number of axioms requiring quantification and to simplify the complexity of problems. While Alt-Ergo offers partial support for the SMT-LIB 2 language, its efficiency with SMT files is comparatively limited.
Main components
The core architecture of Alt-Ergo comprises three main elements: a Depth-First Search (DFS)-based SAT solver, a quantifiers instantiation engine that uses E-Matching, and an assembly of decision procedures for a range of built-in theories. These components collectively enable Alt-Ergo's capabilities in automatic formula solving.
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;[2]
- 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[citation needed];
- 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.
- BWARE[3]
- Cafein[3]
- FUI Hi-Lite[3]
- Decert[3]
- ADT Alt-Ergo[3]
- A3PAT[3]
See also
External links
References
 |  |
