Sound and Complete Proof Rules for Probabilistic Termination

This video presents a research talk from POPL 2025 by Rupak Majumdar and V.R. Sathiyanarayana from MPI-SWS, Germany, addressing the fundamental challenge of proving termination in probabilistic imperative programs. Explore sound and relatively complete proof rules for both qualitative (almost-sure termination) and quantitative (probability bounds) termination problems in programs with discrete probabilistic choice and bounded nondeterminism. Learn how the researchers developed novel proof systems using variant functions as termination distance measures and supermartingales to constrain their growth. Discover how these proof rules can express termination proofs from existing systems and see a practical application through an explicit proof of almost-sure termination for a two-dimensional random walker. The 19-minute presentation was delivered at the ACM SIGPLAN POPL 2025 conference held January 19-25, 2025.