A quantitative probabilistic relational Hoare logic
summary
eRHL is a program logic whose pre/post-conditions are nonnegative real-valued functions on pairs of states, and it gives upper bounds on expectations, probabilities and distances by reasoning about couplings between output distributions. The proof system composes (sequencing, one-sided rules, skip) and isolates probability in a sampling rule. Main results: soundness and relative completeness for all almost-surely terminating programs, completeness for total variation bounds and for epsilon-delta differential privacy, plus rules for loops, recursion and adversaries and worked case studies.
AI-written summary · about
chapters (9)
- 0:00Quantitative probabilistic relational Hoare logic
- 1:06Probabilistic programs and expectations
- 2:54Limitations of relational Hoare logic
- 5:43Introducing quantitative probabilistic logic
- 8:33Proof system and compositionality
- 10:42Soundness and completeness results
- 11:47Corollaries and applications
- 14:55Conclusion and contributions
- 15:40Q&A
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
18mHopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security(…)
21mSeparation Logics for Probability, Concurrency, and Security
21mHyper Separation Logic
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
20mAsynchronous Probabilistic Couplings in Higher-Order Separation Logic
19mMechanized Logical Relations for Termination-Insensitive Noninterference
08mShort Talk: Generalising secure compilation criteria