@article{22102,
  abstract     = {Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of є-DP. Our method refutes є-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for є-DP refutation. To the best of our knowledge, our method is the first method for є-DP refutation to offer the following four desirable features: (1) it is fully automated, (2) it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute є-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.},
  author       = {Chatterjee, Krishnendu and Kafshdar Goharshadi, Ehsan and Zikelic, Dorde},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  keywords     = {Static Program Analysis, Differential Privacy, Probabilistic Programming, Martingales},
  number       = {PLDI},
  publisher    = {Association for Computing Machinery},
  title        = {{SuperDP: Differential privacy refutation via supermartingales}},
  doi          = {10.1145/3808296},
  volume       = {10},
  year         = {2026},
}