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 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, 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
• 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, 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

• Alt-Ergo