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.
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
