Alt-Ergo

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.

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

Several verification platforms are built on Alt-Ergo:

• [http://why3.lri.fr/ Why3], a platform for deductive program verification, uses Alt-Ergo as main prover{{Cite web |title=Why3 |url=https://why3.lri.fr/ |access-date=2023-06-15 |website=why3.lri.fr}}
• 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|date=June 2023}}
• 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 [http://alt-ergo.lri.fr/documents/ABZ-2014.pdf ANR Bware project benchmarks])
• Rodin, a B-method framework developed by Systerel, can use Alt-Ergo as a back-end
• [http://cubicle.lri.fr/ Cubicle], an open source model checker to verify safety properties of array-based transition systems
• [https://www.easycrypt.info/ EasyCrypt], a toolset for reasoning about relational properties of probabilistic computations with adversarial code
• BWARE{{Cite web |title=The Alt-Ergo Theorem Prover: Academic Web Page |url=https://alt-ergo.lri.fr/ |access-date=2023-06-15 |website=alt-ergo.lri.fr}}
• Cafein
• FUI Hi-Lite
• Decert
• ADT Alt-Ergo
• A3PAT

{{Portal|Free and open-source software}}

• Formal verification
• Z3 Theorem Prover

{{Reflist}}

• {{Official website|alt-ergo.ocamlpro.com}}, OcamlPro
• [http://alt-ergo.lri.fr Alt-Ergo at LRI]

{{ML programming}}

Category:OCaml software

Category:Formal methods tools

Category:Software testing tools

Category:Linux software

{{Science-software-stub}}