Programmverifikation

40 Präsenzstunden Vorlesung, 20 Präsenzstunden Übung, 35 Stunden Vor-/Nachbereitung der Übungen, 55 Stunden Nachbereitung der Vorlesung und Prüfungsvorbereitung

Keine

Die Studierenden sind in der Lage

• verschiedene formale Verifikationsmethoden zu erläutern
• formale Verifikationsmethoden auf Beispielprogramme anzuwenden
• formale Programmspezifikationen auf Basis existierender Programme abzuleiten
• moderne Werkzeuge zur Programmverifikation einzusetzen
• zu entscheiden, welche Verifikationsmethodiken für gegebene Aufgaben sinnvoll einsetzbar sind

Für Systeme, deren Versagen menschliches Leben, die Gesundheit oder sehr hohe Vermögenswerte gefährdet (sicherheitskritische Systeme), ist das Vertrauen auf erfolgreiche Tests nicht ausreichend. Verifikation ist der mathematische Beweis, dass ein System gewisse für seine Sicherheit wesentliche Eigenschaften besitzt --- vorausgesetzt Programmeigenschaften werden formal spezifiziert.

Auf einer gemeinsamen theoretischen Basis werden sowohl die klassische Programmverifikation basierend auf dem Hoare Kalkül als auch abstrakte Interpretation und Model Checking betrachtet.

Im Einzelnen

• Grundlagen aus der Logik, Verbände und Fixpunkte
• Formale Spezifikation von Schnittstellen und Abstrakte Datentypen
• Axiomatische Verifikation nach Hoare
• Abstrakte Interpretation nach Cousot
• Software Model-Checking mittels bitpräziser SMT Solver
• Anwendung moderner, in der Industrie eingesetzter Verifikationswerkzeuge
• Begleitung durch Praktikum

Tafel, Folien oder Beamer, live Coding, Moodle, Anwendung realer Werkzeuge

Apt/Olderog; Verification of Sequential and Concurrent Programs; Springer, 1997

Loeckx/Sieber; The Foundations of Program Verification; Teubner; 1987

Müller, Peter; Modular Specification and Verification of Object-Oriented Programs; Springer; 2002

ISBN 3-540-00296-0

Schneider; Verification of Reactive Systems; Springer; 2004;

ISBN 0-521-54310 X

Huth/Ryan; Logic in Computer Science

CACM Computing Surveys, Special Issue on Software Verification, Vol.41 No. 4, 2009

Clarke, Grumberg, Kroening, Peled, Veith: Model Checking 2nd Edition, MIT Press, 2018

Zusätzlich: Aktuelle Online-Quellen und Dokumentationen