Alle Optionen
squeeze  ] [  wheezy  ] [  jessie  ] [  sid  ]
[ Quellcode: alt-ergo  ]

Paket: alt-ergo (0.91-2)

Links für alt-ergo

Screenshot

Debian-Ressourcen:

Quellcode-Paket alt-ergo herunterladen:

Betreuer:

Externe Ressourcen:

Ähnliche Pakete:

Automatischer Theorembeweiser zur Programmverifikation

Alt-Ergo ist ein automatischer Theorembeweiser zur Programmverifikation. Alt-Ergo basiert auf CC(X), einem Kongruenzabschluss-Algorithmus parametrisiert durch eine Gleichungstheorie X. Derzeit kann CC(X) von der leeren Gleichungstheorie und der Linearen Arithmetik instanziiert werden. Alt-Ergo enthält außerdem einen selbsterstellten SAT-Löser und einen Instanziierungsmechanismus.

Alt-Ergo ist sicher und modular: jede Box wird von einem kleinen Satz an Schlussregeln beschrieben und als ein OCaml-Funktor implementiert.

Markierungen: Implementiert in: OCaml, Rolle: Programm

Andere Pakete mit Bezug zu alt-ergo

  • hängt ab von
  • empfiehlt
  • schlägt vor
  • enhances

alt-ergo herunterladen

Download für alle verfügbaren Architekturen
Architektur Paketgröße Größe (installiert) Dateien
amd64 591,9 kB1.820,0 kB [Liste der Dateien]
armel 162,6 kB880,0 kB [Liste der Dateien]
i386 455,3 kB1.252,0 kB [Liste der Dateien]
ia64 163,1 kB880,0 kB [Liste der Dateien]
kfreebsd-amd64 591,3 kB1.800,0 kB [Liste der Dateien]
kfreebsd-i386 454,8 kB1.240,0 kB [Liste der Dateien]
mips 162,7 kB880,0 kB [Liste der Dateien]
mipsel 162,6 kB880,0 kB [Liste der Dateien]
powerpc 554,9 kB1.408,0 kB [Liste der Dateien]
s390 162,6 kB880,0 kB [Liste der Dateien]
sparc 551,8 kB1.424,0 kB [Liste der Dateien]