Alt-Ergo

An SMT Solver for Software Verification


Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat

Download Services Find Out More

Latest News


Releases

Latest Private Release


The latest private release of Alt-Ergo is version 1.20. It was released in February 09, 2016. It is freely available for academia usage. It includes a lot of enhancements and bug fixes compared to latest public release. Don't hesitate to contact us to get access to private releases.


Latest Public Release


The latest public release of Alt-Ergo is version 1.01. It was released in February 16, 2016. It is freely available under the terms of the CeCILL-C license, except for the (OCamlPro) plugins that are provided for a non-commercial purpose only.

Please, follow the links below to download Alt-Ergo, to report a bug, or to ask a question. You may also want to read the CHANGES or see some examples written in Alt-Ergo's native input format.

Sources


(follow instructions in INSTALL.md)

github.com/OCamlPro/alt-ergo

alt-ergo-1.01.tar.gz


Binaries


(without the GUI and the plugins)

Static Linux x86_64 binary

Static Linux x86 binary

Windows-32 binary

OPAM packages


$ opam install alt-ergo
$ opam install altgr-ergo
$ opam install satML-plugin
$ opam install fm-simplex-plugin
$ opam install profiler-plugin



Releases History


public release 1.01
(based on v. 1.00)
February 16, 2016
February 09, 2016 private release 1.20
October 19, 2015 private release 1.10
January 29, 2015 private release 1.00
public release 0.99.1
(based on v. 0.99)
December 30, 2014
January 01, 2014 private release 0.99
public release 0.95.2 September 20, 2013
Alt-Ergo@OCamlPro
public release 0.95.1 March 05, 2013
public release 0.95 January 11, 2013
public release 0.94 December 02, 2011
. . .

Services

Alt-Ergo @ OCamlPro


OCamlPro is investing a lot of time to develop and maintain the Alt-Ergo theorem prover. The aims of this effort are, among others:

  • delivering worldwide and academia users an efficient open source SMT solver for software verification within a basic support to learn how to use it;
  • providing a quality industrial support for developers and industrial users in order to get the best performances from the solver.

We provide two kinds of releases for Alt-Ergo:

Public Releases


Yearly delayed open-source versions: we provide a basic support via our public mailing list and maintain a bugs tracker to centralize eventual issues. These versions are not maintained. So, they are not intended to be used in critical environments.

Private Releases


Up-to-date open-source versions: They are released more frequently. Sources are provided for industrial partners that support our development and for academia users. A javascript version is also provided on this website for world-wide users.

Alt-Ergo at OCamlPro Development Process

Our Support


In order to ease and encourage the integration of Alt-Ergo as a back-end of academic tools, we grant academia users a free access to our latest private versions. Don't hesitate to contact us to get a free access to private releases.

Our clients will have access to the sources of the latest private releases. They will also benefit from our services such as extended developer/production support, dev-on-demand, and re-licensing. Feel free to contact us for more details.

World-Wide Users


  • sources of public releases
  • beginners mailing list
  • bugs tracker
  • online demos of latest releases

Academic Users


  • sources of private releases (Git)
  • users mailing list

Industrial Users


  • sources of private releases
  • developers discussion list
  • developers / production support
  • re-licensing
  • front-line interaction with retailers
  • freezing / maintaining versions
  • qualification kit
  • dev-on-demand


Formal Methods


You have a problem related to formal methods ? You don't know if Alt-Ergo is suitable for your situation ? We can help you to determine the better technology to use for your need.

You are involved in a promising R&D project and you are looking for partners in the field of formal methods ? Our experienced R&D engineers will be happy to contribute to the success of your project. Feel free to contact us to see how we can collaborate.

Online Version


Try-Alt-Ergo is a Javascript version of Alt-Ergo that runs directly in your browser. You don't need to install anything to start using it.


Try-Alt-Ergo Small Tutorial

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.

Alt-Ergo Spider Web


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

Université Paris-Sud LRI INRIA Saclay Ile-de-France CNRS
See publications on alt-ergo.lri.fr