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.

2021W, VU, 4.0h, 6.0EC
Lecture TubeTUWEL

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung
  • LectureTube Lehrveranstaltung
  • 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 link: https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09

 

 

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.13:15 - 15:0019.10.2021 - 18.01.2022 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09 (LIVE)Virtuelle Vorlesung
Do.13:15 - 15:0021.10.2021 - 20.01.2022 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09 (LIVE)Virtuelle Vorlesung
Software Model Checking - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.19.10.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.21.10.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.28.10.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.04.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.09.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.11.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.16.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.18.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.23.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.25.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.30.11.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.02.12.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.07.12.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.09.12.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.14.12.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.16.12.202113:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.11.01.202213:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.13.01.202213:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Di.18.01.202213:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle Vorlesung
Do.20.01.202213:15 - 15:00 https://tuwien.zoom.us/j/91066871404?pwd=aHhNSTl4c1ZWQUtraHdDOW5hcWpCZz09Virtuelle 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
29.09.2021 00:01 30.10.2021 00:59 30.12.2021 23:59

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Vertrautheit mit Aussagenlogik und Prädikatenlogik.

Sprache

Englisch