Title: Verifying Probabilistic Programs: From Theory to Automation

Abstract: Probabilistic programs encode randomized algorithms, robot controllers, learning components, security mechanisms, and much more. They are however hard to grasp. Not only by humans, also by computers: checking elementary properties related to e.g., termination are « more undecidable » than for ordinary programs. The analysis of probabilistic programs requires manipulating irrational or even transcendental numbers. Although this all sounds like a no-go for (semi-)automated analysis, I will present a deductive verification technique to analyse probabilistic programs. In contrast to simulation (like MCMC), this analysis yields exact results. Our technique is based on weakest precondition reasoning. We will explain the foundations of this approach, present some proof rules to reason about probabilistic while-loops, and discuss how the analysis can be automated—either fully or with the help of invariants—and how this is supported by the Ceasar deductive verifier.