EN | DE
Theoretische Informatik

Formale Methoden der Softwareentwicklung

Next offering in Wintersemester 2017/18, previous offering in Wintersemester 2016/17. Please see that webpage, e.g., for details of tools likely to be used in the present edition and for other up-to-date information.

bild_fmsoft_rand.png

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

In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.

The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre- and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.

Literature

  • 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.