# Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs

arXiv: https://arxiv.org/abs/1601.01001 · HTML: https://mlsanity.com/paper/1601.01001/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Jan 2016.

## Built on by (most cited first, 2 of 2)

- [Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems](https://mlsanity.com/paper/2606.17182/) (2026)
- [Quantitative Verification of Omega-regular Properties in Probabilistic Programming](https://mlsanity.com/paper/2512.21596/) (2025)

## Abstract (arXiv)

This paper presents a wp-style calculus for obtaining bounds on the expected run-time of probabilistic programs. Its application includes determining the (possibly infinite) expected termination time of a probabilistic program and proving positive almost-sure termination - does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the run-time of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson's approach for reasoning about the run-time of deterministic programs. We analyze the expected run-time of some example programs including a one-dimensional random walk and the coupon collector problem.