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.

About Licenses & Support Install Documentation Publications Try Online

Latest News

  • Oct 18, 2023 Release of minor version 2.5.2.
  • Sep 14, 2023 Release of minor version 2.5.1.
  • Sep 6, 2023 Release of version 2.5.0.
  • Apr 27, 2023 Release of minor version 2.4.3.
  • Aug 01, 2022 Release of minor version 2.4.2.
  • May 20, 2022 Version 2.3.3 becomes Alt-Ergo-Free 2.3.3.
  • Jul 27, 2021 Release of minor version 2.4.1.
  • Jan 22, 2021 Release of version 2.4.0.
  • Aug 19, 2020 Release of minor version 2.3.3.
  • Jun 2, 2020 Version 2.2.0 becomes Alt-Ergo-Free 2.2.0.
  • Mar 25, 2020 Release of minor version 2.3.2.
  • Feb 19, 2020 Release of minor version 2.3.1.
  • Feb 14, 2020 Second annual meeting of the Alt-Ergo users's club.
  • Jul 7, 2019 Participation to the SMT-COMP : results.
  • More news Find out more.

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

Licenses and Support

Licenses

Alt-Ergo is distributed under three different licenses, depending on the release and support plan:

  • Non Commercial by default: Alt-Ergo is distributed under the OCamlPro-Non-Commercial-License, for research and evaluation purpose only. This license applies to the Alt-Ergo repository on Github;
  • Apache for Gold Plan Only: Gold-level members of the Alt-Ergo's Club receive an Apache Software License version 2.0 on Alt-Ergo, that allows them to redistribute Alt-Ergo as part of their own software;
  • Delayed Free Releases: from time to time, we distribute free releases of Alt-Ergo, that are usually one or two years older than the sources on the Github repository. These releases are licenses under the terms of the CeCILL-C license version 1.

Commercial Support and Sponsoring

OCamlPro provides commercial support on Alt-Ergo for industrial users, and sponsoring as a way to ensure the perennity of the project. This is done as part of the Alt-Ergo's Club with four levels of support. Users from all levels benefit from the access to the chat with developers, logo displayed on this web page and presence at the yearly meeting with the team.

  • Platinum Level: users in this level can distribute Alt-Ergo under the terms of the Apache license v2, taking the master branch or any development branch. They also benefit from 10 days of support, with a 2 work-day reaction time.
  • Gold Level: users in this level can distribute Alt-Ergo under the terms of the Apache license v2, taking only the master branch. They also benefit from 5 days of support, with a 2 work-day reaction time.
  • Silver Level: users in this level cannot distribute Alt-Ergo, but still have unlimited access to the yearly meeting.
  • Bronze Level: users in this level cannot distribute Alt-Ergo, and have a limited access to the yearly meeting to one person.
  • Free Level: users in this level do not benefit from any of the features of our commercial support.

A support plan is subscribed on a yearly basis, and runs until December 31 of the year. Updating from Bronze/Silver level to Gold/Platinum level requires to pay for the new level in full. Updating from Bronze to Silver, or from Gold to Platinum requires only to pay for the difference.

This table provides a simple comparison of support plans:

Platinum Gold Silver Bronze Free
Yearly Price 50 k€ 25 k€ 10 k€ 5 k€
Logo as Sponsor Yes
Licenses
Dev Branches on Github Apache v2 Non-Commercial
Master on Github Apache v2 Non-Commercial
Delayed Free Releases CeCILL-C v1
Support
Included Days of Support 10 5
Reactivity Delay 2 work days
Discussions with developers Email and Chat Email only
Access to Yearly meeting unlimited 1 person

Alt-Ergo Users' Club

The Alt-Ergo Users' Club was launched in 2019, as a way for the Alt-Ergo team to get closer to their users, collect their needs, integrate them in the Alt-Ergo roadmap, and ensure sustainable funding for this project's long-term development.

We are proud to thank the members of the Club, Adacore, Thales, CEA List, MERCE (Mitsubishi Electric R&D Centre Europe) and Trust-In-Soft for their support!

Gold Members

trust-in-soft
thales

Bronze Members

Adacore
Mitsubishi
CEA List

Invited Members

Why3 Team
ENS Paris Saclay

Roadmap of the 2.6.0 release

  • Support for optimization in models of LIA and LRA theories;
  • Ground model checking;
  • Support for the float theory of the SMT-LIB standard;
  • Improve constants propagation for partially interpreted functions.

Join the Club

  • Custom licensing
  • Dedicated support
  • Priority given to your needs
Join The Club!

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.


New Try-Alt-Ergo Blogpost Alt-Ergo Syntax Documentation

The Javascript version is also used as a backend prover in TryWhy3.

Old Version

Try-Alt-Ergo Small Tutorial

Releases

Alt-Ergo is released either under OCamlPro Non-Commercial License (alt-ergo on Opam), either under an Open-Source License with a delay of one or two years (alt-ergo-free on Opam).

Latest Release

The latest release of Alt-Ergo is version 2.5.2. It was released in October 18, 2023. It is available under the terms of the following license.

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

Sources & Binaries

(follow instructions in here to install Alt-Ergo)

github.com/OCamlPro/alt-ergo/tree/v2.5.x

alt-ergo-v2.5.2.tar.gz

Miscellaneous

Commercial Support

Bugs tracker

 

 

OPAM package(s)

$ opam install alt-ergo



Latest Free Release

Alt-Ergo-Free version 2.3.3 was released in May 20, 2022. It is based on Alt-Ergo version 2.3.3, and is available under the terms of the Apache Software License version 2.0.

Sources & Binaries

(follow instructions in INSTALL.md)
github.com/OCamlPro/alt-ergo/tree/2.3.3-free
alt-ergo-free-2.3.3.tar.gz
 

OPAM package(s)

$ opam install alt-ergo-free.2.3.3



Releases History

version 2.5.2 released Oct 18, 2023
version 2.5.1 released Sep 14, 2023
version 2.5.0 released Sep 6, 2023
version 2.4.3 released Apr 27, 2023
version 2.4.2 released Aug 01, 2022
version 2.4.1 released July 27, 2021
July 27, 2021 free version 2.3.0 released
version 2.4.0 released January 21, 2021
version 2.3.3 released August 19, 2020
June 2, 2020 free version 2.2.0 released
version 2.3.2 released March 25, 2020
version 2.3.1 released February 19, 2020
February 13, 2019 free version 2.0.0 released
version 2.3.0 released February 11, 2019
version 2.2.0 released April 21, 2018
version 2.1.0 released March 14, 2018
version 2.0.0 released November 14, 2017
version 1.30 released November 21, 2016
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
. . .

History

  • Jan 21, 2021 Release of version 2.4.0.
  • Feb 13, 2019 First annual meeting of the Alt-Ergo users's club.
  • Feb 13, 2019 Version 2.0.0 becomes Alt-Ergo-Free 2.0.0.
  • Feb 11, 2019 A small recap of what we have done in 2018.
  • Feb 11, 2019 Release of version 2.3.0. See the main CHANGES.
  • April 21, 2018 New release (version 2.2.0) with an experimental support for (a polymorphic extension of) SMT-LIB 2.
  • Mar 14, 2018 New release (v. 2.1.0) with the CDCL solver as a default SAT engine.
  • Nov 14, 2017 New release (v. 2.0.0) with support for floating-point arithmetic.
  • Nov 21, 2016 New release (v. 1.30) with experimental support for models generation.
  • Feb 16, 2016 New public release: private version 1.00 becomes public release 1.01.
  • Feb 09, 2016 A new private version (1.20) and its Javascript version are released.
  • Jan 29, 2015 A new major private release (version 1.00) of Alt-Ergo is released.
  • Jul 15, 2014 Here is a small tutorial about "try Alt-Ergo".
  • Feb 10, 2014 Discover our development/release process scheme !
  • Feb 07, 2014 The latest public release is now available on a Github repository.

Related Publications