Alt-Ergo

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 began in 2006 at the Laboratoire de Recherche en Informatique (LRI), a joint CNRS/Inria unit, at what is now Paris-Saclay University. Since 2013 it has been maintained, developed and distributed by the Formal Methods team at OCamlPro. It is released under the free and open-source software CeCILL-C license.

History The first version of Alt-Ergo was released in 2006. Its architecture was shaped by deductive program verification tools, and it uses a native input language for polymorphic first-order logic that is not compliant with SMT-LIB. OCamlPro announced its support and distribution of the solver in September 2013.

Notable releases include: 2.1.0 (2018): a conflict-driven clause learning (CDCL) SAT solver became the default Boolean reasoner, replacing the earlier tableaux-like approach. 2.2.0 (2018): a new experimental front-end supporting SMT-LIB 2 with a conservative extension for prenex polymorphism. 2.4.0 (2021): support for the incremental commands push and pop from the SMT-LIB standard, and the .ae file extension for the native syntax. 2.5.0 (2022–2023): generation of counterexample models, on a best-effort basis and initially limited to linear arithmetic and enumerated types. 2.6.0 (September 2024): a new relational theory for bit vectors, improvements to the floating-point theory, and the Dolmen library as the default front-end. The release followed an acceleration of development under the DéCySif research project, a collaboration of AdaCore, Inria, OCamlPro and TrustInSoft.

As of October 2026 the project website lists version 2.6.3 (14 April 2026) as the latest release.

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.

Alt-Ergo's native language is a polymorphic first-order logic in the style of ML, and the solver also accepts SMT-LIB v2 input. Since version 2.1.0 its Boolean reasoning has been performed by a CDCL-based SAT solver by default.

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

Licensing and support Alt-Ergo's current releases are distributed under the OCamlPro Non-Commercial License, intended for research and evaluation. Releases are made available under an open-source license after a delay of a few years, published as the alt-ergo-free package, while the current version is the alt-ergo package on opam. OCamlPro offers commercial support to industrial users and funds development partly through the Alt-Ergo Users' Club, a group of supporting organisations. A JavaScript version, Try-Alt-Ergo, runs directly in a web browser.

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 involved in a DO-178C qualification process led by Airbus, during which a qualification kit was produced. 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

Alt-Ergo

Bron en licentie