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

• grundlegende Methoden der Berechnungstheorie anzuwenden um z.B unentscheidbare Probleme zu identifizieren
• fundamentale Methoden der Komplexitätstheorie auf neue Probleme anzuwenden, insb. um zu zeigen ob ein Problem polynomiell lösbar oder NP-schwer ist,
• Probleme aus dem Bereich der formalen Methoden als Erfüllbarkeitsprobleme darzustellen, diese dann mit den entsprechenden Beweissystemen zu  lösen,  sowie die Korrektheit der benutzen Techniken und Reduktionen formal zu argumentieren,
• partielle und vollständige Korrektheit von Softwaresystemen mittels deduktiver Verifikationsansätze basierend auf Hoare Logik und Prädikat-Transfomers formal zu zeigen. Die Studierenden sind außerdem imstande Programsemantiken zu formulieren sowie Programmeigenschaften algorithmisch zu zeigen,
• die grundlegenden Techniken des Model Checking zu verstehen und anzuwenden: das Formulieren von Spezifikationen in Temporallogiken, das Schlussfolgern über Formeln in Temporallogiken, das Model Checking von Formeln auf Kripke Strukturen, das Anwenden von Techniken zur Reduktion des Zustandsraums, und der Einsatz von Bounded Model Checking für Verifikationsprobleme.

Die Lehrveranstaltung behandelt vier Themenblöcke:

1. Grundzüge der Komplexitätstheorie: Problemreduktion, P versus NP, Unentscheidbarkeit;

2. Lösungsmethoden für das aussagenlogische Erfüllbarkeitsproblem (SAT):  Anwendungen in der Informatik;

3. Einführung in die formale Semantik von Programmiersprachen; formale Verifikation von Programmen;

4. Model checking mit Anwendungen in der Hard- und Softwareverifikation.

Didaktisches Vorgehen: Die Vorlesung wird von einer freiwilligen Übung begleitet, in der Aufgaben zu den vier Themenblöcken bearbeitet und zur Korrektur abgegeben werden können. Die Gesamtbeurteilung ergibt sich aus der abschließenden schriftlichen Prüfung.

Die LVA is in 4 Themenblöcke unterteilt. Die LVA (und daher jeder Block) besteht aus einem Vorlesungs- und Vertiefungsteil.

Der Stoff der Lehrveranstaltung wird in den Vorlesungseinheiten präsentiert

Der Vertiefungsteil inkludiert zwei zusätzliche Lehreinheiten, die der Diskussion und dem Lösen von Übungsaufgaben dienen. Studierende erhalten für jeden Themenblock eine Übungssammlung. Ihre Lösungen werden korrigiert um Feedback zu geben.

Drei weitere Einheiten dienen einer Wiederholung grundlegender Techniken zur Beweisführung.

 *********Distance Learning*************

Wegen der COVID-19 Krise wird dieser Kurs online auf TUWEL abgehalten. Studierenden werden Aufzeichnungen der Vorlersung zur Verfügung gestellt und mittels Q+A Sessions (2 pro Block) via Zoom diskutiert. Übungen werden auf TUWEL abgegeben; die Studierenden erhalten Feedback via TUWEL. Die Lösungen werden mittels Q+A Sessions (1 pro Block) via Zoom diskutiert.

Das TUWEL Diskussionsforum wird zur Beantwortung von Fragen und zur Diskussion von Unklarheiten genutzt.

Prüfungsform: Schriftliche Online-Prüfung via TUWEL. Prüfer_innen und Kandidat_innen sind permanent mittels Webmeeting mit Audio und Video verbunden. Die Lösungen können direkt in TUWEL eingegeben oder nach der Prüfung innerhalb einer von der_vom Prüfer_in vorgegebenen Zeit (ca. 5 Minuten) gescannt bzw. abfotografiert und über TUWEL hochgeladen haben.

******************************************

Aufwandsabschätzung

  2 h Einleitung (erste Vorlesung)
 60 h Vorlesung (20 Termine à 2h + 1h Vor-/Nachbereitung)
 40 h Übungsbeispiele (4 Blätter mit je 10 Beispielen à 1h)
 16 h Diskussion der Übungsbeispiele (8 Termine à 2h)
 30 h Testvorbereitung
  2 h schriftlicher Test
-----------------------------------------------------------
150 h = 6 Ects

Die Gesamtbeurteilung erfolgt auf Basis einer schriftlichen Abschlussprüfung.

Folien und Übungsbeispiele siehe TUWEL Online-Kurs.