Probabilistic relational reasoning for differential privacy

DOI10.1145/2103656.2103670zbMath1321.68182OpenAlexW3145555275MaRDI QIDQ2942860

Federico Olmedo, Gilles Barthe, Santiago Zanella Béguelin, Boris Köpf

Publication date: 11 September 2015

Published in: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2103656.2103670

zbMATH Keywords

differential privacyCoq proof assistantrelational Hoare logic

Mathematics Subject Classification ID

Related Items (19)

A denotational semantics for low-level probabilistic programs with nondeterminism ⋮ Understanding Probabilistic Programs ⋮ Product programs and relational program logics ⋮ Unnamed Item ⋮ Verifying Pufferfish privacy in hidden Markov models ⋮ Model checking differentially private properties ⋮ Model Checking Temporal Properties of Recursive Probabilistic Programs ⋮ Divergences on monads for relational program logics ⋮ On the hardness of analyzing probabilistic programs ⋮ Asymmetric Distances for Approximate Differential Privacy ⋮ Toward automatic verification of quantum programs ⋮ Coupled relational symbolic execution for differential privacy ⋮ Graded Hoare logic and its categorical semantics ⋮ Combining Differential Privacy and Mutual Information for Analyzing Leakages in Workflows ⋮ Approximate relational Hoare logic for continuous random samplings ⋮ Preserving differential privacy under finite-precision semantics ⋮ Generalized Differential Privacy: Regions of Priors That Admit Robust Optimal Mechanisms ⋮ Fifty years of Hoare's logic ⋮ Unnamed Item

Uses Software

• Coq

This page was built for publication: Probabilistic relational reasoning for differential privacy