"Hoare Logic"

Models for Probabilistic Programs with an Adversary
Robert Rand, Steve Zdancewic
PDF Slides
Verifying Probabilistic Programs in the Presence of an Adversary
3rd place in the graduate student poster competition.
Robert Rand
Slides Video Poster
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
PDF Cite Slides DOI