VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs
Robert W. Rand, Steve Zdancewic · Electronic Notes in Theoretical Computer Science · 2015
We introduce a Hoare-style logic for probabilistic programs, called VPHL , that has been formally verified in the Coq proof assistant. VPHL features propositional, rather than additive, assertions and a simple set of rules for reasoning about these assertions using the standard axioms of probability theory. VPHL 's assertions are partial correctness assertions , meaning that their conclusions are dependent upon (deterministic) program termination. The underlying simple probabilistic imperative language, PrImp , includes a probabilistic toss operator, probabilistic guards and potentially-non-terminating while loops.