Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification
Owner: Mehdi Dogguy <email@example.com>
* Package name : ergo
Version : 0.7.2
Upstream Author : Sylvain Conchon <firstname.lastname@example.org>
* URL : http://ergo.lri.fr/
* License : CeCILL-C
Programming Lang: OCaml
Description : Automatic theorem prover dedicated to program verification
Ergo is an automatic theorem prover dedicated to program verification.
Ergo is based on CC(X) a congruence closure algorithm parameterized by an
equational theory X. Currently, CC(X) can be instanciated by the empty
equational theory and by the linear arithmetics. Ergo contains also a home
made SAT-solver and an instanciation mechanism.
Ergo is both safe and modular: each box is described by a small set of
inference rules and is implemented as an OCaml functor.
-- System Information:
Debian Release: lenny/sid
APT prefers testing
APT policy: (990, 'testing'), (500, 'unstable')
Architecture: i386 (i686)
Kernel: Linux 2.6.22-3-686 (SMP w/2 CPU cores)
Locale: LANG=fr_FR.UTF-8, LC_CTYPE=fr_FR.UTF-8 (charmap=UTF-8) (ignored: LC_ALL set to fr_FR.UTF-8)
Shell: /bin/sh linked to /bin/bash