Explore a 19-minute conference talk from POPL 2025 that introduces eRHL, a groundbreaking program logic for reasoning about relational expectation properties in probabilistic programs. Learn how this quantitative approach overcomes the randomness alignment restrictions found in previous logics like pRHL and apRHL. Discover why eRHL is the first relational probabilistic program logic with non-trivial soundness and completeness results for almost surely terminating programs. The presentation, delivered by researchers from Centre Inria d'Université Côte d'Azur and MPI-SP/IMDEA Software Institute, demonstrates eRHL's practical benefits through examples that previous logics couldn't handle, while proving its soundness and completeness with respect to program equivalence, statistical distance, and differential privacy. Particularly valuable for those interested in formal verification, Hoare logic, and probabilistic programming.
Overview
Syllabus
[POPL'25] A quantitative probabilistic relational Hoare logic
Taught by
ACM SIGPLAN
Related Courses
-
Hyper Hoare Logic: Proving and Disproving Program Hyperproperties
-
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
-
Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
-
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
-
A Taxonomy of Hoare-Like Logics - Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests
-
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
