KIT | KIT-Bibliothek | Impressum | Datenschutz

Programmverifikationssystem Tatzelwurm. Weiterentwicklung während des KORSO-Projekts

Deussen, Peter; Hansmann, Alexander; Kaeufl, Thomas; Klingenbeck, Stefan

Abstract:

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.


Volltext §
DOI: 10.5445/IR/36495
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1995
Sprache Deutsch
Identifikator urn:nbn:de:swb:90-AAA364955
KITopen-ID: 36495
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,7.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page