Skip to content
Sections
>> Trisquel >> Paquets >> etiona >> math >> alt-ergo
etiona  ] [  nabia  ] [  aramo  ]
[ Paquet source : alt-ergo  ]

Paquet : alt-ergo (1.30+dfsg1-1)

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.

Autres paquets associés à alt-ergo

  • dépendances
  • recommandations
  • suggestions
  • dep: libc6 (>= 2.17)
    GNU C Library: Shared libraries
    un paquet virtuel est également fourni par libc6-udeb
  • dep: libgdk-pixbuf2.0-0 (>= 2.22.0)
    GDK Pixbuf library
  • dep: libglib2.0-0 (>= 2.35.9)
    GLib library of C routines
  • dep: libgmp10
    Multiprecision arithmetic library
  • dep: libgtk2.0-0 (>= 2.24.31)
    GTK+ graphical user interface library
  • dep: libgtksourceview2.0-0 (>= 2.10.0)
    shared libraries for the GTK+ syntax highlighting widget
  • dep: libpango-1.0-0 (>= 1.14.0)
    Layout and rendering of internationalized text
  • dep: zlib1g (>= 1:1.1.4)
    compression library - runtime
  • sug: why
    Software verification tool for C and Java

Télécharger alt-ergo

Télécharger pour toutes les architectures proposées
Architecture Taille du paquet Espace occupé une fois installé Fichiers
amd64 3 025,1 ko16325 ko [liste des fichiers]
i386 2 433,3 ko13327 ko [liste des fichiers]