Model checking differentially private properties

DOI10.1016/J.TCS.2022.10.002OpenAlexW4304080448MaRDI QIDQ2680992FDOQ2680992

Authors: Depeng Liu, Bow-Yaw Wang, Chen Fu, Lijun Zhang 

Publication date: 5 January 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2022.10.002

Recommendations

• Model checking differentially private properties
• Probabilistic relational reasoning for differential privacy
• Deciding differential privacy for programs with finite inputs and outputs
• Differential privacy in probabilistic systems
• The algorithmic foundations of differential privacy

zbMATH Keywords

model checkingdifferential privacytemporal logic

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Differential Privacy
• LightDP: towards automating differential privacy proofs
• The complexity of probabilistic verification
• Probabilistic automata
• Title not available (Why is that?)
• Theory of Cryptography
• Title not available (Why is that?)
• A logic for reasoning about time and reliability
• Model checking of probabilistic and nondeterministic systems
• Title not available (Why is that?)
• A Polynomial-Time Algorithm for the Equivalence of Probabilistic Automata
• An optimal automata approach to LTL model checking of probabilistic systems
• Linear dependent types for differential privacy
• Probabilistic relational reasoning for differential privacy
• Preserving differential privacy under finite-precision semantics
• The algorithmic foundations of differential privacy
• Distance makes the types grow stronger: a calculus for differential privacy
• Formal verification of differential privacy for interactive systems (extended abstract)
• Generalized Bisimulation Metrics
• Universally utility-maximizing privacy mechanisms
• Markov chains and unambiguous Büchi automata
• Bisimilarity distances for approximate differential privacy
• Differential privacy under continual observation
• Proving differential privacy via probabilistic couplings
• Verifying Pufferfish privacy in hidden Markov models
• The big-O problem for labelled Markov chains and weighted automata
• Deciding differential privacy for programs with finite inputs and outputs
• Universally utility-maximizing privacy mechanisms
• Model checking differentially private properties
• Higher-order approximate relational refinement types for mechanism design and differential privacy

Cited In (2)

• Deciding differential privacy for programs with finite inputs and outputs
• Model checking differentially private properties

Uses Software

• PRISM
• PrivateLR
• LightDP
• iscasMc

This page was built for publication: Model checking differentially private properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2680992)