Formale Methoden der Softwareentwicklung ws14

Dozenten Stefan Milius und Tadeusz Litak
Ort Seminarraum 01.150-128, Cauestr. 11
Termine WS2014/2015, Mi 12:15-13:45, Do 8:15-9:45
Umfang Vorlesung+Übung, 4 SWS, ECTS-Credits: 7,5
Beginn Mi, 8. Oktober 2014
Ziel: Werkzeuge für die Korrektheit von Programmen und Systemen
  • Theorie und Praxis automatischer Verfahren zur Korrektheitsprüfung
  • Umgang mit aktuellen Werkzeugen (Dafny, nuSMV) für fehlerfreien Code

Nachrichten

  • In der ersten Woche findet am Mittwoch die Vorlesung von PD Dr. Milius statt. Die Übungen von Dr. Litak beginnen in der zweiten Woche am Mittwoch und die Vorlesung findet ab der zweiten Woche immer donnerstags statt.
  • Material zu Dynamic Frames: Folien, Handout, Paper von I.T.Kassios

Übungen

Please see dedicated webpage for these.

Inhalt

Funktionale Korrektheit von Programmen:

  • Hoare-Kalkül: Vor- und Nachbedindungen, Hoare-Tripel, Schleifeninvarianten
  • Schwächste und schwächste linerale Vorbedingungen
  • Spezifikation von Frame Conditions (Umgang mit Methoden in OO Sprachen)
  • Automatisierung von Korrektheitsbeweisen mit dem Hoare-Kalkül
  • Einfache Beispielprogramme werden erstellt und mit dem verifizierenden Compiler “Dafny” 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

  • M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.
  • K. Rustan M. Leino: Dafny: An automatic program verifier for functional correctness, LPAR 2010 (pdf)