Lower Bounds for Possibly Divergent Probabilistic Programs

Explore a groundbreaking proof rule for verifying lower bounds on quantities of probabilistic programs in this 17-minute conference talk from OOPSLA1 2023. Delve into a novel approach that extends beyond almost-surely terminating programs, enabling the establishment of non-trivial lower bounds on termination probabilities and expected values for potentially divergent probabilistic loops. Examine the application of this rule to complex scenarios, such as the three-dimensional random walk on a lattice. Gain insights into quantitative verification techniques, weakest preexpectations, and the concept of uniform integrability as presented by researchers from various institutions including the Chinese Academy of Sciences, Zhejiang University, Saarland University, and RWTH Aachen University.