  We propose CheckDP, the first automated and integrated approach for proving
or disproving claims that a mechanism is differentially private. CheckDP can
find counterexamples for mechanisms with subtle bugs for which prior
counterexample generators have failed. Furthermore, it was able to
\emph{automatically} generate proofs for correct mechanisms for which no formal
verification was reported before. CheckDP is built on static program analysis,
allowing it to be more efficient and more precise in catching infrequent events
than existing counterexample generators (which run mechanisms hundreds of
thousands of times to estimate their output distribution). Moreover, its sound
approach also allows automatic verification of correct mechanisms. When
evaluated on standard benchmarks and newer privacy mechanisms, CheckDP
generates proofs (for correct mechanisms) and counterexamples (for incorrect
mechanisms) within 70 seconds without any false positives or false negatives.
