  Differential privacy has emerged as a promising probabilistic formulation of
privacy, generating intense interest within academia and industry. We present a
push-button, automated technique for verifying $\varepsilon$-differential
privacy of sophisticated randomized algorithms. We make several conceptual,
algorithmic, and practical contributions: (i) 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 a winning strategy in a game where we have finite privacy resources to
expend. (ii) To discover a winning strategy, we present a constraint-based
formulation of the problem as a set of Horn modulo couplings (HMC) constraints,
a novel combination of first-order Horn clauses and probabilistic constraints.
(iii) We present a technique for solving HMC constraints by transforming
probabilistic constraints into logical constraints with uninterpreted
functions. (iv) Finally, we implement our technique in the FairSquare verifier
and provide the first automated privacy proofs for a number of challenging
algorithms from the differential privacy literature, including Report Noisy
Max, the Exponential Mechanism, and the Sparse Vector Mechanism.
