"Non-termination"

VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs

We introduce a Hoare-style logic for probabilistic programs, called VPHL, that has been formally verified in the Coq proof assistant. …

Robert Rand, Steve Zdancewic