Alt-Ergo

Alt-Ergo
Developer(s)	OCamlPro
Repository	github.com/OCamlPro/alt-ergo ;
Written in	OCaml
Available in	English
Type	Mathematical solver, program verifier
Website	alt-ergo.ocamlpro.com

Alt-Ergo, an automatic solver for mathematical formulas, is mainly used in formal program verification. It operates on the principle of satisfiability modulo theories (SMT). Development was undertaken by researchers at the Paris-Sud University, Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France, and CNRS. Since 2013, project management and oversight has been conducted by OCamlPro company.^[1] It is released under the free and open-source software CeCILL-C license.

Technologies

Design choices

Alt-Ergo employs a specialized input language with prenex polymorphism, designed to reduce the number of axioms requiring quantification and to simplify the complexity of problems. While Alt-Ergo offers partial support for the SMT-LIB 2 language, its efficiency with SMT files is comparatively limited.

Main components

The core architecture of Alt-Ergo comprises three main elements: a depth-first search (DFS)-based SAT solver, a quantifiers instantiation engine that uses e-matching, and an assembly of decision procedures for a range of built-in theories. These components collectively enable Alt-Ergo's abilities in automatic formula solving.

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 data types
AC symbols
Record data types

Industrial uses

Several verification platforms are built on Alt-Ergo:

Why3, a platform for deductive program verification, uses Alt-Ergo as main prover^[2]
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^{[citation needed]}
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 (raising success from 84% to 98% on 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 to verify safety properties of array-based transition systems
EasyCrypt, a toolset for reasoning about relational properties of probabilistic computations with adversarial code
BWARE^[3]
Cafein^[3]
FUI Hi-Lite^[3]
Decert^[3]
ADT Alt-Ergo^[3]
A3PAT^[3]

References

^ "About". alt-ergo.ocamlpro.com. Retrieved 15 June 2023.
^ "Why3". why3.lri.fr. Retrieved 15 June 2023.
^ ^a ^b ^c ^d ^e ^f "The Alt-Ergo Theorem Prover: Academic Web Page". alt-ergo.lri.fr. Retrieved 15 June 2023.