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 mittels Vorlesungsvideos präsentiert
Der Vertiefungsteil inkludiert pro Block drei zusätzliche Präsenz-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 Vorlesungs-Einheiten dienen einer Wiederholung grundlegender Techniken zur Beweisführung.
Sollte CoVID-bedingt eine Umstellung von Präsenz auf Online notwendig werden, gibt es folgende Änderungen:
- Prüfung: Wird verschoben oder online in Tuwel statt in Präsenz
- Q+A Sessions via Zoom
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
