Der Einsatz von formalen Methoden bei der Softwareentwicklung bietet eine Möglichkeit die
Sicherheit von Software, gegenüber dem herkömmlichen Testen, zu vergrößern.
Kernstück einer solchen Entwurfsmethode ist ein formaler Beweis, daß ein Programm seine Spezifikation erfüllt.
In diesem Beitrag werden Methoden vorgestellt mit denen ein solcher Korrektheitsbeweis automatisiert werden kann.
Es wird der Einsatz von Ternärvektorlisten als zentrale Datenstruktur für boolesche Ausdrücke vorgeschlagen.
Inhalt:/ Content: Institut für Informatik
TU Bergakademie Freiberg
Gestaltung/ Layout: Webmaster
19. Februar 1997
