Alt-Ergo

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

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[edit]

Design choices[edit]

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[edit]

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[edit]

Alt-Ergo implements (semi-)decision procedures for the following theories:

Industrial uses[edit]

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.

External links[edit]