Alt-Ergo
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 the Why's
syntax. 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.91)
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.