Automated Verification meets Differential Privacy
Talkat Data Privacy: From Foundations to Applications (Simons Institute workshop, 2019) · 2019-03-04..03-08·
summary
Automatic verifier transforms sampling into assume statements, encodes failure probability as a program variable, and hands the result to off‑the‑shelf SMT/SAT solvers to discharge proofs; simple algorithms (report noisy max and a Laplace accuracy proof) verify in about 22 seconds, and a synthesizer rediscovers an iterative database construction algorithm from a few examples in minutes. The system discovers coupling strategies for ε‑DP, composes Laplace‑centered axioms, uses union‑bound style accumulation, and currently handles pure ε (not (ε,δ)) with engineered axioms for distributions.
AI-written summary · about
chapters (4)
related talks
21mModular Verification of Differential Privacy in Probabilistic Higher-Order Separation(…)
58mAutomating Relational Verification of Infinite-State Programs
27mAutomated Learning and Verification of Embedded Security Architectures
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
54mVerification Dilemmas, Law, and the Promise of Zero-Knowledge Proofs
06mFormal Verification with the Certora Prover
28mProving Obliviousness of Probabilistic Algorithms with Formal Verification
27mVerified Differential Privacy for Finite Computers