Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
For researchers and practitioners in probabilistic program verification, this work provides a novel representation that drastically reduces computational overhead, enabling verification of larger programs.
The authors developed typed extended decision diagrams (TEDDs) to address the explosion of logical representations in weakest pre-expectation computations for probabilistic programs. Their method improves scalability by orders of magnitude over existing deductive verification approaches.
Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these quantitative expectations. Their automation has been successful in analysing a variety of discrete probabilistic programs. Key routines in that automation require reasoning about (partially unrolled) loops, however, the logical representation of weakest pre-expectations on such unrollings often explodes. In this paper, we develop typed extended decision diagrams (TEDDs), inspired by various extensions to binary decision diagrams. We demonstrate computing WPs represented as TEDDs, SMT-based pruning to further shrink their representation, and we lift some proof rules to operate on TEDDs. Finally, we demonstrate that TEDDs boost the scalability of deductive probabilistic program verification by orders of magnitudes over the state of the art.