Bug#468557: ITP: ergo -- Automatic theorem prover dedicated to program verification

[Mehdi Dogguy <Mehdi.Dogguy@pps.jussieu.fr>]

Package: wnpp
Severity: wishlist
Owner: Mehdi Dogguy <dogguy@pps.jussieu.fr>


* Package name    : ergo
  Version         : 0.7.2
  Upstream Author : Sylvain Conchon <conchon@lri.fr>
* 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