Please subscribe to the StudOn course for the present edition, e.g., for details of tools likely to be used and for other up-to-date information.

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. The difference with other lectures covering similar material is that instead of a plain imperative language, we focus on languages dealing with shared mutable data structures and involving  constructs like allocation or deallocation. In other words, our Hoare formalism is (concurrent or heap-based) separation logic.

Furthermore, unlike SemProg we focus on push-button tools rather than approaches based on proof assistants.

• G. Winskel: The Formal Semantics of Programming Languages: An Introduction, The MIT Press, 1993.
• Ch. Baier, J-P. Katoen, Principles of Model Checking, The MIT Press, 2008.
• M. Huth, M. Ryan: Logic in Computer Science, Cambridge University Press, 2. Aufl., 2004.