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 verpflichtenden Übung begleitet, in der Aufgaben zu den vier Themenblöcken zu bearbeiten und bei vier Abgabegesprächen zu präsentieren sind. Die Gesamtbeurteilung ergibt sich aus den Abgabegesprächen und der abschließenden schriftlichen Prüfung.
Die Gesamtbeurteilung ergibt sich aus den Leistungen, die bei den Übungsblättern zu den vier Themengebieten (jeweils max. 10 Punkte) sowie beim schriftlichen Abschlusstest (max. 60 Punkte) erbracht werden. Insgesamt können somit 4*10+60=100 Punkte erzielt werden. Für eine positive Gesamtbeurteilung sind mindestens 20 Punkte bei den Übungsblättern und 30 Punkte beim Abschlusstest erforderlich. Positive Noten ergeben sich aus der Gesamtpunktezahl nach folgendem Schlüssel:
- 50-61 Punkte: genügend
- 62-74 Punkte: befriedigend
- 75-87 Punkte: gut
- 88-100 Punkte: sehr gut
