Alt-Ergo is an open source automatic theorem prover dedicated to program verification. It is an SMT solver based on CC(X): a congruence closure algorithm parameterized by an equational theory X. Alt-Ergo is based on a home-made SAT-solver and implements an instantiation mechanism for quantified formulas. Its architecture is summarized by the the following picture.
Alt-Ergo is highly modular. Each box is described by a small set of inference rules and is implemented as an Ocaml functor. Alt-Ergo's input syntax is described here. You will find here a bunch of examples. Currently, Alt-Ergo provides a built-in support for the following theories:
- the free theory of equality with uninterpreted symbols,
- linear arithmetic over integers and rationals,
- non-linear arithmetic,
- polymorphic functional arrays,
- enumerated datatypes,
- record datatypes,
- associative and commutative (AC) symbols,
- fixed-sized bit-vectors.