Alt-Ergo

Alt-Ergo is an automatic solver for mathematical formulas, specifically designed for program verification. It is based on satisfiability modulo theories (SMT) and distributed under an open-source license (CeCILL-C). Alt-Ergo was developed by researchers at Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France, and CNRS. Alt-Ergo has been overseen by the OCamlPro company since 2013.[1]

Alt-Ergo
Developer(s)OCamlPro
Repository
TypeMathematical solver, program verifier
Websitehttps://alt-ergo.ocamlpro.com

Technologies

Design choices

Alt-Ergo employs a specific input language with prenex polymorphism. This language helps to reduce the number of quantified axioms and the complexity of problems. Alt-Ergo also partially supports the SMT-LIB 2 language, but is less efficient when dealing with 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:

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;[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;
  • 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.
  • BWARE[3]
  • Cafein[3]
  • FUI Hi-Lite[3]
  • Decert[3]
  • ADT Alt-Ergo[3]
  • A3PAT[3]

See also

References
  1. "About". alt-ergo.ocamlpro.com. Retrieved 2023-06-15.
  2. "Why3". why3.lri.fr. Retrieved 2023-06-15.
  3. "The Alt-Ergo Theorem Prover: Academic Web Page". alt-ergo.lri.fr. Retrieved 2023-06-15.


This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.