About
What is Alt-Ergo ?
Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. It is based on Satisfiability Modulo Theories (SMT). Solvers of this family have made impressive advances and became very popular during the last decade. They are now used is various domains such as hardware design, software verification and formal testing.
What is Alt-Ergo Good for ?
Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why platform. Currently, it is used as a back-end of different tools and in various settings, in particular via the Why3 platform. For instance, the Frama-C suite relies on it to prove formulas generated from C code, and the SPARK toolset uses it to check formulas produced from Ada programs. In addition, Alt-Ergo is used to prove formulas issued from B modelizations and from cryptographic protocols verification. The figure given below shows the main tools that rely on Alt-Ergo to prove the formulas they generate.
You are using Alt-Ergo in another context/tool not cited above ? Let us know !
Under the Hood
Alt-Ergo's native input language is a polymorphic first-order logic "à la ML" modulo theories. This logic is very suitable for expressing formulas generated in the context of program verification. It also provides a support of the SMT-LIB v2 standard input format. Currently, Alt-Ergo is capable of reasoning in the combination of the following built-in theories:
- the free theory of equality with uninterpreted symbols,
- linear arithmetic over integers and rationals,
- fragments of non-linear arithmetic,
- polymorphic functional arrays with extensionality,
- enumerated datatypes,
- record datatypes,
- associative and commutative (AC) symbols,
- fixed-size bit-vectors with concatenation and extraction operators.
Origins
Alt-Ergo results from academic researches conducted conjointly at Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France and CNRS since 2006. Publications and theoretical foundations are available on its academic web page. Since September 2013, Alt-Ergo is maintained and distributed by the OCamlPro company. Academic researches are now conducted in collaboration with the VALS team of LRI.
See publications on Alt-Ergo back then at lri.fr, now Laboratoire Méthodes Formelles (CNRS-Inria).
The DéCySif joint research project
DéCySif is a regional R&D project that aims at improving the safety and security of critical systems using formal verification tools. The project is funded by an i-Démo call and the Ile-de-France French Region, gathering 4 partners: AdaCore, Inria, OCamlPro and TrustInSoft.
See the DéCySif project's website
