Alt-Ergo is an automatic solver for mathematical formulas, specifically designed for program verification. It is based on satisfiability modulo theories (SMT) and distributed under an open-source license (CeCILL-C). Alt-Ergo was developed by researchers at Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France, and CNRS. Alt-Ergo has been overseen by the OCamlPro company since 2013.
Technologies
Design choices
Alt-Ergo employs a specific input language with prenex polymorphism. This language helps to reduce the number of quantified axioms and the complexity of problems. Alt-Ergo also partially supports the SMT-LIB 2 language, but is less efficient when dealing with 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
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; 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. BWARE Cafein FUI Hi-Lite Decert ADT Alt-Ergo A3PAT