69 lines
2.7 KiB
Markdown
69 lines
2.7 KiB
Markdown
---
|
|
title: "Alt-Ergo"
|
|
chunk: 1/1
|
|
source: "https://en.wikipedia.org/wiki/Alt-Ergo"
|
|
category: "reference"
|
|
tags: "science, encyclopedia"
|
|
date_saved: "2026-05-05T12:13:04.106916+00:00"
|
|
instance: "kb-cron"
|
|
---
|
|
|
|
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. 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
|
|
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 (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
|
|
Cafein
|
|
FUI Hi-Lite
|
|
Decert
|
|
ADT Alt-Ergo
|
|
A3PAT
|
|
|
|
|
|
== See also ==
|
|
|
|
Formal verification
|
|
Z3 Theorem Prover
|
|
|
|
|
|
== References ==
|
|
|
|
|
|
== External links ==
|
|
Official website, OcamlPro
|
|
Alt-Ergo at LRI |