CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples
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 …