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.

@article{paperbot2044,
  title = {Lower Bounds for Possibly Divergent Probabilistic Programs},
  author = {Shenghua Feng and Mingshuai Chen and Han Su and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Naijun Zhan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {OOPSLA1},
  year = {2023},
  doi = {10.1145/3586051}
}