Alt-Ergo

This article contains content that is written like an advertisement. Please help by removing promotional content and inappropriate external links, and by adding encyclopedic content written from a neutral point of view. (March 2015) (Learn how and when to remove this template message)

This article does not cite any sources. Please help by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources:  –  ·  ·  · scholar · JSTOR (November 2014) (Learn how and when to remove this template message)

Alt-Ergo

Developer(s)	OCamlPro
Repository	github.com/OCamlPro/alt-ergo
Type	Mathematical solver, program verifier
Website	http://alt-ergo.lri.fr

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

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
• floating point arithmetic

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.

See also[]

• Formal verification
• Z3 Theorem Prover

External links[]

• Alt-Ergo at LRI
• Alt-Ergo at OcamlPro

This scientific software article is a stub. You can help Wikipedia by .

• v
• t