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.

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

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.

Vorbesprechung: 8.10.2019, 9:15 EI8

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.

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.