# Bounded Model Checking for Probabilistic Programs

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

## Key facts

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

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

- [Abstraction-Refinement for Hierarchical Probabilistic Models](https://mlsanity.com/paper/2206.02653/) (2022)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Value Iteration with Guessing for Markov Chains and Markov Decision Processes](https://mlsanity.com/paper/2505.06769/) (2025)

## Abstract (arXiv)

In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard probabilistic program is a potentially infinite parametric Markov decision process, no direct adaption of existing techniques is possible. Therefore, we propose an on-the-fly approach where the operational model is successively created and verified via a step-wise execution of the program. This approach enables to take key features of many probabilistic programs into account: nondeterminism and conditioning. We discuss the restrictions and demonstrate the scalability on several benchmarks.