ws15 fmsoft

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

  • Slides of Lecture 1, Oct 13 (password protected)
  • Slides of Lecture 2, Oct 21 (password protected)
  • From lecture 3 on, lectures are given entirely on blackboard, so you can only rely on your notes for this.
  • However, I had some introductory slides used in lecture 9 on the frame problem and reasoning about shared mutable data structures. Available freely, without password.

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.

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.