Fri 12 Jan 2018 14:05 - 14:30 at Watercourt - Probability Chair(s): Lars Birkedal

In this paper, we present a push-button, automated technique for verifying $\epsilon$-differential privacy of sophisticated randomized algorithms. We make a range of conceptual, algorithmic,and practical contributions: (1) Inspired by the recent advances on approximate couplings and randomness alignment, we present a new proof technique called coupling strategies, which casts differential privacy proofs as discovering a strategy in a game where we have finite privacy resources to expend. (2) To discover a winning strategy, we present a constraint-based formulation of the problem as solving a set of Horn modulo couplings (HMC) constraints, a novel kind of constraints combining first-order Horn clauses with probabilistic constraints. (3) We present a technique for solving HMC constraints by transforming probabilistic constraints into logical constraints with uninterpreted functions. (4) Finally, we implement our technique and provide the first automated proofs of a number of algorithms from the differential privacy literature, including Report Noisy Max, the Exponential Mechanism, and the Sparse Vector Mechanism.

#### Fri 12 Jan

 13:40 - 15:20: Research Papers - Probability at Watercourt Chair(s): Lars BirkedalAarhus University 13:40 - 14:05Talk Proving expected sensitivity of probabilistic programsGilles BartheIMDEA Software Institute, Thomas EspitauUniversite Pierre et Marie Curie, Benjamin GregoireINRIA, Justin HsuUniversity College London, Pierre-Yves StrubEcole Polytechnique 14:05 - 14:30Talk Synthesizing Coupling Proofs of Differential PrivacyAws AlbarghouthiUniversity of Wisconsin-Madison, Justin HsuUniversity College London 14:30 - 14:55Talk Measurable cones and stable, measurable functionsThomas EhrhardCNRS and University Paris Diderot, Michele PaganiUniversity Paris Diderot, Christine TassonUniversity Paris Diderot 14:55 - 15:20Talk Denotational validation of higher-order Bayesian inferenceAdam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Ohad KammarUniversity of Oxford, Matthijs VákárUniversity of Oxford, Sam StatonUniversity of Oxford, Hongseok YangUniversity of Oxford, Yufei CaiUniversity of Tuebingen, Klaus OstermannUniversity of Tuebingen, Sean K. MossUniversity of Cambridge, Chris HeunenUniversity of Edinburgh, Zoubin GhahramaniUniversity of Cambridge