Formale Verifikation von ANSI-C Programmen

Frage
der Informatik. Nicht nur für sicherheitskritische Anwendungen sind
Beweise
über die Korrektheit von Programmen von hoher Bedeutung. Dennoch wird in
der
Praxis, also von der Softwareindustrie, kaum gebrauch von formalen
Methoden
zur Verifikation von Software Gebrauch gemacht. Ein wichtiger Beitrag
zur
Akzeptanz formaler Methoden zur Verifikation von Software ist die
eingesetzte Programmiersprache. Im industriellen Umfeld ist die Sprache
ANSI-C von überragender Bedeutung. Die Sprache gilt wegen ihrer
komplizierten Semantik als ungeeignet für die formale Verifikation. In
meinem Vortrag stelle ich eine Hoare-Axiomatisierung von Teilen von
ANSI-C
vor. Diese Formalisierung wird verwendet um ein Theorembeweissystem als
Prototyp zu implementieren. Die Interaktion, die das Theorembeweissystem
erlaubt, wird verwendet, um das große, unhandliche Gesamtproblem in
mehrere,
kleinere Teilproblem aufzuteulen. Desweiteren stelle ich
Entscheidungsalgorithmen vor, die solche Teilprobleme automatisiert
lösen
können.