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 steer autonomous robots and self-driving cars, are key to describe security mechanisms, naturally encode randomized algorithms, and are rapidly encroaching AI and machine learning.

This tutorial will present recent developments on the formal verification of probabilistic programs. We will focus on syntax-based program verification and survey weakest precondition-style reasoning on discrete probabilistic programs. These techniques can be used to determine quantitative properties of a program such as the probability of divergence, bounds on the expected outcomes of program expressions, or the program’s expected run-time. Several examples will be used to illustrate the approach, and methods for automated verification will be discussed.