Programmverifikationssystem Tatzelwurm. Weiterentwicklung während des KORSO-Projekts

Der Bericht enthält eine kurze Darstellung der Entwicklungsarbeiten,
die im Rahmen des KORSO-Projekts erfolgt sind. Eine
Versionsverwaltung erlaubt den Einsatz des Verifikationssystems
während der Programmentwicklungsphase. Zum Beweis der in allen
Phasen der Softwareentwicklung anfallenden Verifikations-
bedingungen wurde der Beweiser erheblich weiterentwickelt. Der
Benutzer hat die Möglichkeit, eigene Beweisregeln zu definieren.
Eine Sprache zur Formulierung von Beweisplnen erleichtert die
während der Entwicklung von korrekter Software oftmals notwendige
Wiederholung von Beweisen. Mit Hilfsmitteln zur Erzeugung von
Gegenbeispielen bei unbeweisbaren Formeln erhält der Anwender
nützliche Hinweise zur Lokalisierung von Fehlern.