Misplaced Pages

Alt-Ergo

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
SMT solver for software verification
This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.
Find sources: "Alt-Ergo" – news · newspapers · books · scholar · JSTOR (July 2023) (Learn how and when to remove this message)

Alt-Ergo
Developer(s)OCamlPro
Repository
Written inOCaml
Available inEnglish
TypeMathematical solver, program verifier
Websitealt-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. 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:

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

References

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

External links

ML programming
Software
Implementations,
dialects
Caml
Standard ML
Dependent ML
Programming tools
  • Alt-Ergo°
  • Astrée
  • Camlp4°
  • FFTW°
  • Frama-C°
  • Haxe°
  • Marionnet°
  • MTASC°
  • Poplog°
  • Semgrep°
  • SLAM project
    • Theorem provers,
    proof assistants
    Community
    Designers
  • Lennart Augustsson (Lazy ML)
  • Damien Doligez (OCaml)
  • Gérard Huet (Caml)
  • Xavier Leroy (Caml, OCaml)
  • Robin Milner (ML)
  • Don Sannella (Extended ML)
  • Don Syme (F#)
  • Italics = discontinued
  • ° = Open-source software
    Book Category:Family:ML Category:Family:OCaml Category:Software:OCaml
    • Stub icon

    This scientific software article is a stub. You can help Misplaced Pages by expanding it.

    Categories: