Survey Lecture: Joost-Pieter Katoen: The Surprises of Probabilistic Termination

Thursday, July 01, 2021, 4:30pm

Speaker: Joost-Pieter Katoen



Program termination is a key question in program verification. This talk considers the termination of probabilistic programs, programs that can describe e.g., randomized algorithms, security algorithms and Bayesian learning.

Probabilistic termination has several nuances. Diverging program runs may occur with probability zero. Such programs are almost surely terminating (AST). If the expected duration until termination is finite, they are positive AST.

This talk presents the different nuances of probabilistic termination and discusses the hardness (how undecidable are these notions?) to check these properties.

To conclude we will present a simple proof rule for deciding AST, and reports on recent approaches towards automation to check whether a program is AST, PAST, non-AST, non-PAST, or “don’t know”.


The talks of the UnRAVeL survey lecture 2021 will be given via Zoom every Thursday from 16:30 to 18:00:


Meeting ID: 960 4371 5437

Passcode: 039217