Probabilistic relational reasoning for differential privacy
DOI10.1145/2103656.2103670zbMATH Open1321.68182OpenAlexW3145555275MaRDI QIDQ2942860FDOQ2942860
Authors: Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin 
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
Recommendations
- Coupled relational symbolic execution for differential privacy
- Distance makes the types grow stronger: a calculus for differential privacy
- Deciding differential privacy for programs with finite inputs and outputs
- LightDP: towards automating differential privacy proofs
- Proving differential privacy via probabilistic couplings
Online algorithms; streaming algorithms (68W27) Randomized algorithms (68W20) Cryptography (94A60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cited In (34)
- Generalized differential privacy: regions of priors that admit robust optimal mechanisms
- Relational \(\star\)-liftings for differential privacy
- Divergences on monads for relational program logics
- Asymmetric Distances for Approximate Differential Privacy
- \(*\)-liftings for differential privacy
- Product programs and relational program logics
- Approximate relational Hoare logic for continuous random samplings
- Graded Hoare logic and its categorical semantics
- Combining Differential Privacy and Mutual Information for Analyzing Leakages in Workflows
- Proving differential privacy via probabilistic couplings
- On the hardness of analyzing probabilistic programs
- Distance makes the types grow stronger: a calculus for differential privacy
- Fifty years of Hoare's logic
- Formal verification of differential privacy for interactive systems (extended abstract)
- Understanding probabilistic programs
- Higher-order approximate relational refinement types for mechanism design and differential privacy
- On Differentially Private Inductive Logic Programming
- Linear dependent types for differential privacy
- Deciding differential privacy for programs with finite inputs and outputs
- Verifying Pufferfish privacy in hidden Markov models
- Coupled relational symbolic execution for differential privacy
- Title not available (Why is that?)
- Model checking differentially private properties
- LightDP: towards automating differential privacy proofs
- Does a Program Yield the Right Distribution?
- Logical foundations of quantitative equality
- Model checking differentially private properties
- A denotational semantics for low-level probabilistic programs with nondeterminism
- Title not available (Why is that?)
- Preserving differential privacy under finite-precision semantics
- Proving that programs are differentially private
- Toward automatic verification of quantum programs
- Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs
- Differential privacy in probabilistic systems
Uses Software
This page was built for publication: Probabilistic relational reasoning for differential privacy
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942860)
