Formale Methoden und Werkzeuge

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