185.A93 Formale Methoden der Informatik
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2019W, UE, 2.0h, 3.0EC

Merkmale

  • Semesterwochenstunden: 2.0
  • ECTS: 3.0
  • Typ: UE Übung

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

  • ... Probleme als SAT oder SMT Probleme zu formalisieren,
  • ... diese Formalisierungen mittels Z3 zu lösen,
  • ... ein kombinatorisches Problem mittels einer Reduktion und einem SAT-solver zulösen,
  • ... deduktive Verifikationsmethoden anzuwenden, die auf Hoare-Logik und Predikat-Transformatoren basieren,
  • ... um die teilweise/vollständige Korrektheit von Software mithilfe deduktiver Überprüfungsmethoden und -werkzeuge festzustellen,
  • ... Model Checking anzuwenden: ein Model des zu verifizierenden Systems zu erstellen, die Spezifikation in einer temporallogischen Formel zu formulieren, und mögliche Gegenbeispiele zu interpretieren.

Inhalt der Lehrveranstaltung

Diese Lehrveranstaltung vertieft das Verständnis der Inhalte der Lehrveranstaltung "6.0 VU Formale Methoden der Informatik" durch zusätzliche Übungen. Es werden Aufgaben zu folgenden Gebieten behandelt:

  • Komplexitätstheorie: NP-Vollständigkeit, Unentscheidbarkeit, Reduktion von Problemen
  • Erfüllbarkeitsprobleme: SAT, SMT
  • Partielle/Totale Korrektheit von Programmen: Hoare-Kalkül, schwächste Vorbedingung, stärkste Nachbedingung
  • Formale Verifikation mittels Model Checking

Methoden

Zu jedem der vier Themenblöck gibt es ein Übungsblatt.

  • Das Übungsblatt wird in einer Vorlesungseinheit vorgestellt.
  • Die Übungsaufgaben sind von den Studierenden selbständig zu bearbeiten und die Lösungen in tuwel hochzuladen.
  • Die Lösungen werden in einer abschließenden Einheit besprochen.

Prüfungsmodus

Prüfungsimmanent

Weitere Informationen

Vorbesprechung: 8.10.2019, 9:15 EI8

Vortragende

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Di.09:00 - 10:0008.10.2019EI 8 Pötzl HS Vorbesprechung
Di.08:00 - 10:0015.10.2019 - 28.01.2020EI 8 Pötzl HS Übungen
Formale Methoden der Informatik - Einzeltermine
TagDatumZeitOrtBeschreibung
Di.08.10.201909:00 - 10:00EI 8 Pötzl HS Vorbesprechung
Di.15.10.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.22.10.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.29.10.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.05.11.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.12.11.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.19.11.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.26.11.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.03.12.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.10.12.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.17.12.201908:00 - 10:00EI 8 Pötzl HS Übungen
Di.07.01.202008:00 - 10:00EI 8 Pötzl HS Übungen
Di.14.01.202008:00 - 10:00EI 8 Pötzl HS Übungen
Di.21.01.202008:00 - 10:00EI 8 Pötzl HS Übungen
Di.28.01.202008:00 - 10:00EI 8 Pötzl HS Übungen

Leistungsnachweis

Die eingereichten Lösungen der vier Übungsblätter werden jeweils mit 0-15 Punkten bewertet. Hierbei werden neben der Korrektheit der Lösung auch die Qualität & Verständlichkeit des dazugehörigen Reports bewertet. Die Note ergibt sich aus der Summe dieser Punkte.

LVA-Anmeldung

Von Bis Abmeldung bis
06.10.2019 00:00 05.11.2019 00:00 05.11.2019 00:00

Curricula

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Es wird vorrausgesetzt das die  VU Formale Methoden der Informatik parallel besucht wird (oder schon in einem früheren Semester absolviert wurde). DIe Übungsblöcke bauen auf den Inhalen der dazugehörigen Vorlesungsblöcken auf.

 

Begleitende Lehrveranstaltungen

Sprache

bei Bedarf in Englisch