Alt-Ergo is an automatic solver for mathematical formulas, specifically designed for program verification. It is based on
satisfiability modulo theories
In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvi ...
(SMT) and distributed under an open-source license (CeCILL-C). Its original authors were Sylvain Conchon and Evelyne Contejean, a
LRI but it is now developed and maintained a
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
The SAT ( ) is a standardized test widely used for college admissions in the United States. Since its debut in 1926, its name and scoring have changed several times; originally called the Scholastic Aptitude Test, it was later called the Schola ...
, 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
In computing, floating-point arithmetic (FP) is arithmetic that represents real numbers approximately, using an integer with a fixed precision, called the significand, scaled by an integer exponent of a fixed base. For example, 12.345 can be r ...
* 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
Frama-C stands for ''Framework for Modular Analysis of C programs''. Frama-C is a set of interoperable program analyzers for C programs. Frama-C has been developed by the French Commissariat à l'Énergie Atomique et aux Énergies Alternativ ...
, a framework to analyse C-code, uses Alt-Ergo in the Jessie and WP plugins (dedicated to "deductive program verification");
*
SPARK
Spark commonly refers to:
* Spark (fire), a small glowing particle or ember
* Electric spark, a form of electrical discharge
Spark may also refer to:
Places
* Spark Point, a rocky point in the South Shetland Islands
People
* Spark (surname)
* ...
, 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 th
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.
See also
*
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
*
Z3 Theorem Prover
External links
Alt-Ergo at OcamlProAlt-Ergo at LRI
OCaml software
Formal methods tools
Software testing tools
Linux software
{{science-software-stub