This article contains content that is written like an advertisement. (March 2015) (Learn how and when to remove this template message)
This article does not cite any sources. (November 2014) (Learn how and when to remove this template message)
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.
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.
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.
Alt-Ergo implements (semi-)decision procedures for the following theories:
- empty theory
- linear integer arithmetic
- linear rational arithmetic
- non-linear arithmetic
- polymorphic arrays
- enumerated datatypes
- AC symbols
- record datatypes
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.
|This software article is a stub. You can help Wikipedia by expanding it.|