Wahlvorlesung im Bachelorstudium Informatik
Lernziele
Wesentliche Methoden und Werkzeuge zum exakten
Formulieren und Nachweisen von Eigenschaften von
Softwaresystemen kennen, verstehen, auswählen, anwenden.
Den Zusammenhang zu den zugrundeliegenden fundamentalen
Ideen verstehen, die bereits aus anderen Vorlesungen bekannt
sind (VL Modellierung: Logik, VL Automaten und formale
Sprachen: Automaten, VL (Fortgeschrittene) Programmierung:
Termersetzung, Lambda-Kalkül, Typsysteme).
Lehrinhalte
- SAT-Solver und BDDs als aussagenlogische Werkzeuge
- Beschreibung des Systemverhaltens durch aussagenlogische
Formeln (bounded model checking)
- Werkzeuge zur programmatischen Herstellung solcher
Formeln (Bsp: ersatz)
- Werkzeuge zu effizienten Bestimmung eines Modells
(SAT-Solver, Bsp: kissat)
- Werkzeuge zur Darstellung und effizienten Verarbeitung
von Modellmengen als Boolesche Entscheidungsdiagramme
(BDD),
- Model Checking mit endlichen Automaten
- Beschreibung des Systemverhaltens durch eingeschränkte
prädikatenlogische Formeln
- effiziente Operationen auf endlichen Automaten, die
Modellmengen darstellen
- Programmierwerkzeuge für präzise Typisierung
- die Curry-Howard-Isomorphie (Typ = Aussage, Programm =
Beweis)
- Programmiersprachen mit dependent types (Bsp: Agda)
- interaktive Beweis-Systeme (Bsp: Mimer für Agda)
Literatur
- Cerone, A., Roggenbach, M., Schlingloff, B.-H.,
Schneider, G., Shaikh, S.A.: Teaching formal methods for
software engineering - ten principles, Informatica
Didactica, Nr. 9, (2015). https://www.informaticadidactica.de/uploads/Artikel/Schlinghoff2015/Schlinghoff2015.pdf
- Uwe Schöning, Jacob Toran: Das Erfüllbarkeitsproblem
SAT, Lehmanns (2012)
- Christel Baier, Joost Katoen: Principles of Model
Checking. MIT Press, Cambridge (2008)
- Samuel Mimram: Program = Proof, https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/course.pdf
Software (Auswahl)
- Edward Kmett et al.: ersatz, A monad for expressing SAT
or QSAT problems using observable sharing. 2010–, https://hackage.haskell.org/package/ersatz
- Johannes Waldmann: boumchak Bounded Model Checker,
2017–, https://git.imn.htwk-leipzig.de/waldmann/boumchak
- Armin Biere: The Kissat SAT Solver, 2022–, https://github.com/arminbiere/kissat
- Ulf Norell, Andreas Abel, et al.: Agda, 2005–, https://wiki.portal.chalmers.se/agda/
Organisatorisches
- Vorlesung mit Übung
- Prüfungszulassung: regelmäßiges und erfolgreiches
Bearbeiten von Übungsaufgaben
- Prüfung: Klausur