This program is tentative and subject to change.

Mon 16 Jan 2023 09:00 - 10:30 at Copley - Tutorials 4A
Mon 16 Jan 2023 11:00 - 12:30 at Copley - Tutorials 4B

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.

This program is tentative and subject to change.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Tutorials 4ATutorialFest at Copley
09:00
90m
Tutorial
Deductive Verification of Probabilistic Programs
TutorialFest
Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja Technical University of Denmark
11:00 - 12:30
Tutorials 4BTutorialFest at Copley
11:00
90m
Tutorial
Deductive Verification of Probabilistic Programs
TutorialFest
Benjamin Lucien Kaminski Saarland University and University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja Technical University of Denmark