After successful completion of the course, students are able to...
a. have an acquaintenance with the core concepts of probabilistic programming:
sampling, conditioning, and querying.
b. be familiar with the probabilistic programming language WebPPL.
c. have a thorough understanding of the semantics of probabilistic programs.
d. know deductive verification techniques for proving elementary properties of probabilistic programs such as termination, expected outcomes, and expected runtimes.
e. have a basic understanding of the relationship with Bayesian networks.
f. have rudimentary knowledge on core verification topics such as loop invariants
The lecturer of this course will be Prof. Joost-Pieter Katoen / RWTH Aachen University (D) and University of Twente (NL).
Course abstract: Probabilistic programs feature sampling from probability distributions and the ability to condition values of variables in a program. The latter feature distinguishes modern probabilistic programming languages such as WebPPL, Pyro, Edward, Scenic, from those in the early days describing randomized algorithms.
Although probabilistic programs are normal–looking programs, reasoning about their correctness is intricate. They do not generate a single output but a distribution over outputs. Whereas a classical program terminates or not, this is no longer true for probabilistic programs.
They can diverge, but this may happen with probability zero. That is, even if programs terminate with probability one, they may have non-terminating runs.
Establishing correctness of probabilistic programs needs—even more so than ordinary programs—formal reasoning. In this course, we will introduce probabilistic programs, their formal semantics, elementary decision problems and their complexity, and focus on the deductive verification of such programs.
Outline course content (subject to changes):
1. Introduction and WebPPL (2 hours)
2. pGCL: Syntax and Markov Semantics (2 hours)
3. Fixed Points and Dijkstra's Weakest Preconditions (2 hours)
4+5. Probabilistic Weakest Precondition Reasoning (4 hours)
6. Termination (2 hours)
7. Expected Runtime Analysis (2 hours)
8. Verifying Bayesian Networks (2 hours)
9. Probabilistic Separation Logic (2 hours)
10. Towards the Automated Verification of Probabilistic Programs (2 hours)
