Lower Bounds for Possibly Divergent Probabilistic Programs


We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs – as is the case for existing rules – and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.

Proc. ACM Program. Lang., 7(OOPSLA1)
Mingshuai Chen
Mingshuai Chen
ZJU100 Young Professor

My research interests include formal verification, programming theory, and logical aspects of computer science.