Will my program terminate? If initially x == 2, will x be even after program termination? These are qualitative problems in program verification with answers either yes or no, true or false. In this tutorial, 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? Can I answer these questions also if my program had access to randomness?

In this tutorial, 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.