Symbolic Execution for Probabilistic Programs: Path Probabilities Testing and Verification in PRISM Model Checker

Randomized algorithms are ubiquitous, yet reasoning about their outcome probabilities remains a challenging task. This thesis presents a framework that symbolically executes randomized programs to enumerate all feasible execution paths and compute path probabilities as closed-form expressions over program parameters. These path probabilities are aggregated to derive overall probabilities of user-defined outcomes such as assertions, program states, or events. To validate the analysis, the framework automatically generates equivalent PRISM models from the computed path probabilities. These auto-generated models are executed and their results are compared with the outcomes of the corresponding hand-crafted PRISM implementations of the same benchmark programs. The close numerical agreement between the two PRISM results (typically within 10^-9) confirms that the framework’s probability computations are semantically correct.

The framework is evaluated on canonical benchmarks, including the Monty Hall problem, Freivalds’ algorithm, Monte Carlo pi estimation (looping), the Birthday Paradox, and the Von Neumann Fair Coin from a Biased Coin, which cover branching structures, loops, and parameterized randomness.

Experimental results demonstrate:

(i) exact probability derivations where feasible, 

(ii) scalable approximations for loops using bounded unrolling or geometric closure, and (iii) automated cross-verification with PRISM. Overall, the system enables explainable and formally validated probability reasoning for randomized programs, aiding both debugging and assurance of probabilistic correctness.

Committee: Liyi Li (major professor), Myra Cohen, and Samik Basu