192.106 Software Model Checking
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2020W, VU, 4.0h, 6.0EC
TUWEL

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Distance Learning

Lernergebnisse

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.

Inhalt der Lehrveranstaltung

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.

Methoden

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

Prüfungsmodus

Mündlich

Weitere Informationen

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

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.15:00 - 17:0006.10.2020 - 15.12.2020 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.14:00 - 16:0009.10.2020 - 18.12.2020 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Software Model Checking - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.06.10.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.09.10.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.13.10.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.16.10.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.20.10.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.23.10.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.27.10.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.30.10.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.03.11.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.06.11.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.10.11.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.13.11.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.17.11.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.20.11.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.24.11.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.27.11.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.01.12.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.04.12.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Fr.11.12.202014:00 - 16:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung
Di.15.12.202015:00 - 17:00 Siehe Vorlesungsankündigung und Folien "Introduction", Seite 35Software Model Checking Vorlesung

Leistungsnachweis

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.

 

LVA-Anmeldung

Von Bis Abmeldung bis
30.09.2020 00:01 30.10.2020 23:59 31.12.2020 23:59

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Vertrautheit mit Aussagenlogik und Prädikatenlogik.

Sprache

Englisch