SuperDP: Differential privacy refutation via supermartingales Chatterjee, Krishnendu ; https://orcid.org/0000-0002-4561-241X Kafshdar Goharshadi, Ehsan ; https://orcid.org/0000-0002-8595-0587 Zikelic, Dorde ; https://orcid.org/0000-0002-4681-1699 Static Program Analysis Differential Privacy Probabilistic Programming Martingales ddc:000 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. Association for Computing Machinery 2026 info:eu-repo/semantics/article doc-type:article text http://purl.org/coar/resource_type/c_2df8fbb1 https://research-explorer.ista.ac.at/record/22102 https://research-explorer.ista.ac.at/download/22102/22135 Chatterjee K, Goharshady E, Zikelic D. SuperDP: Differential privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>. 2026;10(PLDI). doi:<a href="https://doi.org/10.1145/3808296">10.1145/3808296</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1145/3808296 info:eu-repo/semantics/altIdentifier/e-issn/2475-1421 info:eu-repo/semantics/altIdentifier/arxiv/2603.26215 info:eu-repo/semantics/openAccess