article published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Ehsan Kafshdar Goharshadi author 103b4fa0-896a-11ed-bdf8-87b697bef40d0000-0002-8595-0587 Dorde Zikelic author 294AA7A6-F248-11E8-B48F-1D18A9856A870000-0002-4681-1699 KrCh department Formal Methods for Stochastic Models: Algorithms and Applications project 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. https://research-explorer.ista.ac.at/download/22102/22135/2026_ProcACMProgrammingLanguages_Chatterjee.pdf application/pdfno Association for Computing Machinery2026 eng Static Program AnalysisDifferential PrivacyProbabilistic ProgrammingMartingales 2475-1421 2603.2621510.1145/3808296 10PLDI https://research-explorer.ista.ac.at/record/22134 K. Chatterjee, E. Goharshady, and D. Zikelic, “SuperDP: Differential privacy refutation via supermartingales,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI. Association for Computing Machinery, 2026. Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218. Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2026. <a href="https://doi.org/10.1145/3808296">https://doi.org/10.1145/3808296</a>. Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI, 218, Association for Computing Machinery, 2026, doi:<a href="https://doi.org/10.1145/3808296">10.1145/3808296</a>. Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href="https://doi.org/10.1145/3808296">https://doi.org/10.1145/3808296</a> K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (2026). 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> 221022026-06-21T22:02:59Z2026-06-24T06:39:37Z