Programmverifikation
Name Programmverifikation
Verantwortlich Prof. Dr. Matthias Güdemann
SWS 4
ECTS 5
Sprache(n) Deutsch (Standard)
Englisch
Lehrform SU mit Praktikum
Angebot im Wechsel mit anderen Fächern der gleichen Fachgruppe
Aufwand

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

Voraussetzungen

Keine

Ziele

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
Inhalt

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
Medien und Methoden

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

Literatur

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

Zuordnungen Curricula
SPO Fachgruppe Code ab Semester Prüfungsleistungen
IG Version 2010 VCML: Theoretische Grundlagen IG-TTI-0090 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2010 EC: Theoretische Grundlagen IG-TTI-0090 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2010 SWE: Theoretische Grundlagen IG-TTI-0090 1 benotete schriftliche Prüfung 90 Minuten
IG Version 2019 EC: Theoretische Grundlagen IG-TTI-0090 1 mündliche Prüfung
schriftliche Prüfung
IG Version 2019 SWE: Theoretische Grundlagen IG-TTI-0090 1 mündliche Prüfung
schriftliche Prüfung
IG Version 2019 VCML: Theoretische Grundlagen IG-TTI-0090 1 mündliche Prüfung
schriftliche Prüfung