Topic of the course: Techniques and tools for proving the correctness of programs and systems

• Theory and application of automated correctness verification methods
• Working with tools used to test for bugs in software

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.

In both parts of the course we will be working with verification tools based on the theoretical material presented during the lecture. The exact tools used may vary from year to year; for the first part, we have used model checkers such as NuSMV and Spin in the past, while tools for the second part have included Dafny, Frama-C and VeriFast.

• 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.
• O’Hearn, Peter. Separation logic. Communications of the ACM 62, no. 2 (2019): 86-95.