Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage Software Model Checking Werkzeuge einzusetzen und zu implementieren. Kursabsolventen sind mit dem aktuellen Stand der Wissenschaft im Bereich Software Model Checking und insbesonderen den relevanten Algorithmen vertraut, können Software Model Checking Werkzeuge in einfachen Projekten einsetzen und deren Nutzen in komplexen Projekten abschätzen. Des Weiteren werden Studierende in der Lage sein, ein einfaches Model Checking Werkzeug selbst zu implementieren.
Grundlagen
Der erste Teil der Vorlesung beschäftigt sich mit Semantik und der Enkodierung von Transitionsrelationen.
- Einleitung und Motivation: Übersicht über die Kursinhalte, die Notwendigkeit von automatischer Verifikation
- Ein kleiner Schritt für einen Menschen: Small step semantics, Hoare Logik und Predikatentransformer, Kripke Strukturen und Transitionsrelationen.
Teil I
Von einzelnen Transitionsschritten zum Bounded Model Checking, Erreichbarkeit und Temporallogikeigenschaften, Berechnung von Fixpunkten.
Teil II: Bis zur Unendlichkeit und noch viel weiter
In diesem Teil beschäftigen wir uns damit, wie die Konzepte aus dem ersten Teil verwendet werden können, um Programme mit potenziell unendlich großem Zustandsraum zu verifizieren. Dieser Teil beschäftigt sich mit statischer Analyse, Prädikatenabstraktion, interpolationsbasiertem Model Checking, und Model Checking von parallelen Programmen.
In diesem Kurs wird eine Mischung aus folgenden Lehrmethoden eingesetzt:
- Frontalvorträge
- selbstständiges Erarbeiten von Inhalten wissenschaftlicher Publikationen
- Arbeiten mit Verifikationswerkzeugen
- Implementierung von vorgestellten Algorithmen
