Tutorial speaker Joost-Pieter Katoen
Joost-Pieter Katoen is full professor at the RWTH Aachen University in the Software Modeling and Verification (MOVES) group and part-time associated to the Formal Methods & Tools group at the University of Twente. His research areas includes formal methods, computer-aided verification—in particular model checking—, concurrency theory, probabilistic computation, and semantics. Joost-Pieter Katoen is ACM Fellow and holder of an ERC Advanced Research Grant.
Talk
Verifying Probabilistic Programs: From Theory to Automation
Tuesday, 16:30
Room: Auditorium
Probabilistic programs describe recipes on how to infer conclusions about big data from a mixture of uncertain data and real-world observations. Bayesian networks, a key model in decision-making, are simple instances of such programs. Probabilistic programs are used to steer autonomous robots and self-driving car, are key to describe security mechanisms, and naturally encode randomized algorithms. Due to their learning ability, they are rapidly encroaching AI and probabilistic machine learning.
This tutorial will consist of two parts. The first part focuses on syntax-based verification of discrete probabilistic programs. We will show how weakest pre-condition style reasoning can be used to determine quantitative program properties such as the probability of divergence, bounds on the expected outcomes of program expressions, or the program’s expected run-time. The second part will focus on possible automation. We will present automated methods such as k-induction and how to find loop invariants in a CEGIS-like fashion. An outlook will be given of some alternative automated techniques for program equivalence and how to exploit model checking in the analysis of probabilistic programs.