Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism. Its architecture is summarized by the the following picture.

Alt-Ergo is both safe and modular: each box is described by a small set of inference rules and is implemented as an Ocaml functor. Moreover, the code is short (7000 lines for the whole program but just 4500 for the main loop).

How to use it

Alt-Ergo's input syntax is described here. You will find here a bunch of examples.

Bibliography

Project Leaders

Sylvain Conchon
Evelyne Contejean

Team members

François Bobot
Mohamed Iguernelala
Stéphane Lescuyer
Alain Mebsout

Download


Latest version (0.94) CHANGES
Alt-Ergo is freely available, under the terms of the CeCILL-C LICENSE. It is available as:

Contact

Subscribe to the users mailing list to ask questions about Alt-Ergo or to get announces of new releases etc.