EN | DE
Theoretische Informatik

Formale Methoden der Softwareentwicklung

Dozenten Dr Tadeusz Litak und Christoph Rauch
Umfang Vorlesung+Übung, 4 SWS, ECTS-Credits: 7,5

The dates are temporary, please consult UniViS for up to date information. As far as I see, at the moment most likely ones are:

V/UE; 4 SWS; ECTS: 7,5; Gasthörer; Di, 12:15 - 13:45, 00.152-113; Mi, 16:00 - 17:30 (we start 15 mins earlier, at participants' request!)

Contrary to original plans, Priv. Doz. Milius will not be giving this lecture. The change of the main lecturer to dr Litak entails as least two important changes:

  • The lecture will be given in English
  • Dafny, which appeared in the original course description, will be replaced by another Hoare-reasoning tool, most likely based on separation logic. Details will follow.

Lecture slides

The password for the first two items was announced at the October 28 lecture. If you still need it, email me.

Tutorials

Please see dedicated webpage for these.

Ariane

Ziel: Werkzeuge für die Korrektheit von Programmen und Systemen
  • Theorie und Praxis automatischer Verfahren zur Korrektheitsprüfung
  • Umgang mit aktuellen Werkzeugen für fehlerfreien Code

Inhalt

Funktionale Korrektheit von Programmen:

  • Hoare-Kalkül: Vor- und Nachbedindungen, Hoare-Tripel, Schleifeninvarianten
  • Schwächste und schwächste liberale Vorbedingungen
  • Automatisierung von Korrektheitsbeweisen mit dem Hoare-Kalkül
  • Einfache Beispielprogramme werden erstellt und verifiziert

Formale Verifikation reaktiver Systeme:

  • Temporallogiken: CTL, LTL, CTL-Stern
  • Spezifikation von Systemeigenschaften (Safety und Liveness)
  • Fixpunktcharakterisierung von CTL
  • Modelprüfung reaktiver Systeme
  • Einfache Systemmodelle und Spezifikationen werden in nuSMV erstellt und verifiziert

Literatur

  • G. Winskel: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.
  • M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.