1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
Source: alt-ergo
Section: math
Priority: optional
Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
Uploaders:
Mehdi Dogguy <mehdi@debian.org>,
Ralf Treinen <treinen@debian.org>
Build-Depends:
debhelper (>= 10),
ocaml-nox (>= 3.12.1),
ocaml-findlib,
libocamlgraph-ocaml-dev (>= 1.8.5~),
liblablgtk2-gnome-ocaml-dev (>= 2.14.0+dfsg-2~),
liblablgtksourceview2-ocaml-dev (>= 2.14.0+dfsg-2~),
libzarith-ocaml-dev,
libzip-ocaml-dev,
ocplib-simplex-ocaml-dev,
dh-ocaml (>= 0.9.0~)
Homepage: http://alt-ergo.lri.fr
Standards-Version: 3.9.8
Vcs-Browser: https://anonscm.debian.org/cgit/pkg-ocaml-maint/packages/alt-ergo.git
Vcs-Git: https://anonscm.debian.org/git/pkg-ocaml-maint/packages/alt-ergo.git
Package: alt-ergo
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}, ${ocaml:Depends}
Suggests: why
Description: Automatic theorem prover dedicated to program verification
Alt-Ergo is an automatic theorem prover geared towards application in
program verification. It is based on CC(X), a congruence closure
algorithm parameterized by an equational theory X. Alt-Ergo has
built-in provers for propositional logic, linear arithmetic,
uninterpreted function symbols, associative-commutative function
symbols, polymorphic arrays, user-defined polymorphic record types
and polymorphic enumeration types. It has restricted support for
reasoning over arbitrary user-defined algebraic types, first-order
quantifiers, and non-linear arithmetic.
.
This package contains the prover as a command-line executable
as well as the graphical interface.
|
