(* An OCaml SMT-solver for software verification *) 

 
 

Overview

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's architecture

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.
 

Download


Latest release

Alt-Ergo is freely available under the terms of the CeCILL-C licence. The latest release (0.95.1) was published on March 05th, 2013. It is available as:


What's new in this release


This minor release mainly fixes some bugs and issues reported by users.

What's new in Alt-Ergo 0.95


  • Main changes in the solver:
    • a new combination method for Shostak solvers,
    • improvement of distribution of non-linear multiplication over addition,
    • input language extension: polymorphic declaration are now allowed (logic x: 'a),
    • input language extension: the types of terms can now be forced in a formula using the construct <term> : <type> (see man for an example),
    • input language modification: a label should be a string. The construct <label> : <term> is replaced by "<label>" : <term>,
    • new keywords in the syntax: inversion, check, cut and include,
    • experimental options for theories models generation: -model option for model on labeled terms and -complete-model option for a complete model,
    • -timelimit n option: set the time limit to n seconds (not supported on Windows),
    • bug fixes.
  • Main changes in the graphical interface:
    • the number of instances for each axiom are now shown on the right of the GUI,
    • the number of instances of each axiom can be limited by the user,
    • the modifications made in the GUI can now be saved in a session file <f>.agr,
    • session files can be replayed with -replay option,
    • models can be displayed in the GUI,
    • unsat-cores (-proof option) can be used to simplify the context.

Compatibility


It has been reported that Alt-Ergo (version >= 0.95) is not compatible with the Oxygen release of Frama-C.

Previous versions


You can still access the previous versions of Alt-Ergo here.
 

Contact


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