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

Diese Vorlesung wird in Englisch und online abgehalten.

Zoom Meetings Dienstag:

Meeting ID: 954 1816 7847
Password: SoMoCh20

https://tuwien.zoom.us/j/95418167847?pwd=eTZ1aEE4R3dOQ2Z5VFZIaU9xem1mdz09

Zoom Meetings Freitag:

Meeting ID: 983 6354 2656
Password: SoMoCh20

https://tuwien.zoom.us/j/98363542656?pwd=VDRKZEk3enZzTlVCNkxNYUJ4eWh0Zz09

Die Note setzt sich zu gleichen Teilen aus einer Note für den Übungsteil (Implementierung eines Model Checkers mit Abgabegespräch) und einer Note für eine mündliche Prüfung (Fragen zum theoretischen Teil im Rahmen des Abgabegesprächs) zusammen.

Vertrautheit mit Aussagenlogik und Prädikatenlogik.