SPEAKER: Benjamin Kaminski (Saarland University)

Will my program terminate? If initially x == 2, will x be even after program termination? These are qualitative problems in program verification and answers to these questions are either yes or no, true or false. In order to make our life more difficult (but also much more interesting), we will study how to measure quantities instead of truth: How long will it take until my program terminates? Given the input value, what output value will my program produce? Given an observed output value, what was the input value? What can I still say if my program had access to randomness? In this course, we will investigate how to reason about such quantitative properties of software, i.e. typically infinite-state systems described symbolically by some programming language. To that end, we will first study qualitative deductive reasoning via Dijkstra's weakest [liberal] preconditions and strongest postconditions. We will then gradually lift qualitative to quantitative weakest pre / strongest post transformers. In particular, we will learn how to interpret weakest pre and strongest post meaningfully in a quantitative setting. We will also learn about a concept that Dijkstra missed to investigate (or did not care to investigate): strongest liberal post[conditions]. Finally, we will have a look at weakest pre transformers for probabilistic programs. We will learn how to use these transformers to reason about reachability probabilities and expected values. We will also learn how to adapt the probabilistic weakest pre calculus in order to reason about expected runtimes of probabilistic programs.

PREREQUISITES: Basics of FO logic and ideally also of Hoare logic. Basic knowledge of complete lattices is also beneficial.