alt-ergo - Automatic theorem prover dedicated to program verification

Property Value
Distribution Debian 8 (Jessie)
Repository Debian Main amd64
Package name alt-ergo
Package version 0.95.2
Package release 3
Package architecture amd64
Package type deb
Installed size 9.19 KB
Download size 1.51 MB
Official Mirror
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.


Package Version Architecture Repository
alt-ergo_0.95.2-3_i386.deb 0.95.2 i386 Debian Main
alt-ergo - - -


Name Value
libatk1.0-0 >= 1.12.4
libc6 >= 2.14
libcairo2 >= 1.2.4
libfontconfig1 >= 2.11
libfreetype6 >= 2.2.1
libgdk-pixbuf2.0-0 >= 2.22.0
libglib2.0-0 >= 2.35.9
libgmp10 -
libgtk2.0-0 >= 2.24.0
libgtksourceview2.0-0 >= 2.10.0
libpango-1.0-0 >= 1.14.0
libpangocairo-1.0-0 >= 1.14.0
libpangoft2-1.0-0 >= 1.14.0


Type URL
Binary Package alt-ergo_0.95.2-3_amd64.deb
Source Package alt-ergo

Install Howto

  1. Update the package index:
    # sudo apt-get update
  2. Install alt-ergo deb package:
    # sudo apt-get install alt-ergo




2014-04-27 - Mehdi Dogguy <>
alt-ergo (0.95.2-3) sid; urgency=medium
* Remove previously introduced patch since relevant API change
has been reverted in OCamlgraph 1.8.5.
- Remove 0002-Port-to-OCamlgraph-1.8.4.patch
- Build-Depend on OCamlgraph >= 1.8.5~.
2014-03-30 - Mehdi Dogguy <>
alt-ergo (0.95.2-2) sid; urgency=medium
* Port to OCamlgraph 1.8.4 (Closes: #743072)
- add 0002-Port-to-OCamlgraph-1.8.4.patch
2013-11-17 - Ralf Treinen <>
alt-ergo (0.95.2-1) sid; urgency=low
* New upstream release.
* Update debian/watch, now points to ocamlpro site.
* Refresh patch 0001-No-need-to-activate-debug-flag.patch
* Drop patch 0002-Do-not-run-the-test-if-test.mlw-is-absent-and-use-be.patch:
the file test.mlw is no longer relevant.
* drop patches that have been applied by upstream:
- 0003-Fix-a-typo.patch
- 0004-Add-rules-and-targets-for-gui.byte.patch
- 0005-Look-for-cma-instead-of-cmxa-for-lablgtksourceview2.patch
- 0007-Fix-all-target.patch
- 0008-Split-install-pack-into-two-separate-targets-opt-and.patch
- 0009-clean-remove-META.patch
* Add build-dependency on libzarith-ocaml-dev
* debian/rules:
- drop backup of .depend which is no longer needed
- drop overwrite for dh_auto_configure
- in dh_auto_build target, drop touching of configure
* debian/copyright:
- update Download field to ocamlpro
- Upstream Contact : add alt-ergo-bugs mailing list
- Update copyright holder and year for files *
- Put paragraphs into the right order
* install examples/ into /usr/share/doc/alt-ergo
* Standards-version 3.9.5 (no change)
2013-08-24 - Ralf Treinen <>
alt-ergo (0.95.1-3) unstable; urgency=low
* make libalt-ergo-ocaml-dev conflict and replace with alt-ergo (<<
0.95.1-1) to resolve file conflict with versions of the package before
the split into two binary packages (closes: #718010).
2013-05-10 - Ralf Treinen <>
alt-ergo (0.95.1-2) unstable; urgency=low
* upload to unstable

See Also

Package Description
alt-key_2.2.5-2_amd64.deb tool to help developers improve keyboard accelerators
altermime_0.3.10-7_amd64.deb utility used to alter mime-encoded mailpacks
altos_1.5-1_amd64.deb Altus Metrum firmware and utilities
altree-examples_1.3.1-2_all.deb example files for ALTree
altree_1.3.1-2+b1_amd64.deb program to perform phylogeny-based association and localization analysis
alure-doc_1.2-6_all.deb AL Utilities REtooled (documentation)
alure-utils_1.2-6_amd64.deb AL Utilities REtooled (utilities)
am-utils-doc_6.2+rc20110530-3.2_all.deb automounter utilities documentation
am-utils_6.2+rc20110530-3.2_amd64.deb automounter utilities from 4.4BSD (includes amd)
amanda-client_3.3.6-4_amd64.deb Advanced Maryland Automatic Network Disk Archiver (Client)
amanda-common_3.3.6-4_amd64.deb Advanced Maryland Automatic Network Disk Archiver (Libs)
amanda-server_3.3.6-4_amd64.deb Advanced Maryland Automatic Network Disk Archiver (Server)
amap-align_2.2-4_amd64.deb Protein multiple alignment by sequence annealing
amarok-common_2.8.0-2.1_all.deb architecture independent files for Amarok
amarok-doc_2.8.0-2.1_all.deb Amarok documentation (Handbook)