./wip/alt-ergo, Automatic theorem prover for program verification

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 1.01, Package name: alt-ergo-1.01, Maintainer: MarkoSchuetz

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.


Required to run:
[lang/ocaml] [devel/nspr] [x11/ocaml-lablgtk] [devel/ocamlgraph]

Required to build:
[pkgtools/x11-links] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [x11/xorgproto]

Master sites:

Version history: (Expand)

CVS history: (Expand)


   2015-07-10 14:37:44 by Thomas Klausner | Files touched by this commit (1) | Package updated
Log message:
Update HOMEPAGE and MASTER_SITES, but the distfile doesn't fetch for me.
0.99.1 update is available.
   2015-07-10 11:49:26 by Thomas Klausner | Files touched by this commit (1) 
Log message:
Update path to ocamlgraph.
   2014-10-10 16:03:21 by Thomas Klausner | Files touched by this commit (3) 
Log message:
Update for lablgtk -> ocaml-lablgtk rename.
   2012-09-24 18:56:26 by Aleksej Saushev | Files touched by this commit (144) 
Log message:
Drop superfluous PKG_DESTDIR_SUPPORT, "user-destdir" is default these days.
Mark packages that don't and might probably not have staged installation.
   2011-05-21 21:14:41 by Marko Schütz Schmuck | Files touched by this commit (4) 
Log message:
initial commit