• Hauptseite
• Software
• Berichte
• Verifikation
• Demonstrator
• Veröffentlichungen
• Kontakt

Software

Aktuelle Versionen

• Die Schutzfeldberechnung als Bücherei.

Die Verifikationsumgebung besteht aus zwei Komponenten, welche hier heruntergeladen werden können:

• Die Isabelle-Theorien, welche den eigentlichen Korrektheitsbeweis ermöglichen, und
• das C-Frontend, welches annotierte C-Programme nach Isabelle übersetzt.

Für die Isabelle-Theorien wird Isabelle 2009 benötigt, für das C-Frontend der Haskell-Compiler und Cabal.

Alte Versionen

Diese werden aus historischen und Referenzgründen zur Verfügung gestellt, und werden nicht mehr unterstützt.

Version 0.96

Diese Version beinhaltet eine zusammengefasste Spezifikation der Berechnung der Sicherhheitszonen.

• Die Schutzfeldberechung (nur der reine Quellcode; besser nutzbar ist die Bücherei oben).
• Die Beweisdokumente. Um sie laufen zu lassen, werden die Theorien der Entwicklungsumgebung und Isabelle 2009 benötigt.

Version 0.9

Dies ist die Version, die dem TÜV zur Verfügung gestellt wurde, und die Grundlage der Zertifizierung war:

• Die Schutzfeldberechung (nur der reine Quellcode; besser nutzbar ist die Bücherei oben).
• Die Beweisdokumente. Um sie laufen zu lassen, werden die Theorien der Entwicklungsumgebung und Isabelle 2009 benötigt.
• Das C-Frontend (benötigt zum Übersetzen ghc 6.10).