[{"publisher":"ACM","OA_place":"publisher","related_material":{"record":[{"status":"public","relation":"research_data","id":"22134"}]},"date_created":"2026-06-21T22:02:59Z","title":"SuperDP: Differential privacy refutation via supermartingales","article_processing_charge":"Yes","file_date_updated":"2026-06-24T06:19:56Z","arxiv":1,"ec_funded":1,"issue":"PLDI","ddc":["000"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"oa_version":"Published Version","external_id":{"arxiv":["2603.26215"]},"article_number":"218","date_updated":"2026-09-16T07:36:14Z","PlanS_conform":"1","license":"https://creativecommons.org/licenses/by/4.0/","language":[{"iso":"eng"}],"keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"das_tickbox":"1","volume":10,"corr_author":"1","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","orcid":"0000-0002-8595-0587"},{"orcid":"0000-0002-4681-1699","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","last_name":"Zikelic"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2026","supplementarymaterial":"no","abstract":[{"lang":"eng","text":"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."}],"publication":"Proceedings of the ACM on Programming Languages","researchdata_availability":"yes","quality_controlled":"1","acknowledgement":"The authors would like to thank Petr Novotný for valuable discussions that helped shape this work.\r\nThis research was supported by the Singapore Ministry of Education (MOE) Academic Research\r\nFund (AcRF) Tier 1 grant (Proposal ID: 25-SIS-SMU-009), Vienna Science and Technology Fund\r\n(WWTF), State of Lower Austria [Grant ID 10.47379/ICT25017], ERC CoG 863818 (ForM-SMArt),\r\nand Austrian Science Fund (FWF) 10.55776/COE12.","_id":"22102","month":"06","oa":1,"OA_type":"gold","dataavailabilitystatement":"The artifact supporting the findings of this study, which includes the underlying datasets, software\r\ncode, and experiments, is publicly available in Zenodo https://zenodo.org/records/19399862.","project":[{"call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"Bilateral Artificial Intelligence (Chatterjee)","_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","grant_number":"COE12"}],"intvolume":"        10","day":"08","type":"journal_article","fulldoi":"https://doi.org/10.1145/3808296","publication_status":"published","scopus_import":"1","file":[{"file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","checksum":"994bf21d6269dabccf1e1091e02962c5","success":1,"file_id":"22135","relation":"main_file","date_updated":"2026-06-24T06:19:56Z","content_type":"application/pdf","file_size":858595,"date_created":"2026-06-24T06:19:56Z","creator":"dernst","access_level":"open_access"}],"has_accepted_license":"1","doi":"10.1145/3808296","citation":{"apa":"Chatterjee, K., Goharshady, E., &#38; Zikelic, D. (2026). SuperDP: Differential privacy refutation via supermartingales. <i>Proceedings of the ACM on Programming Languages</i>. ACM. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>","ieee":"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. ACM, 2026.","ama":"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>","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, and Dorde Zikelic. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>. ACM, 2026. <a href=\"https://doi.org/10.1145/3808296\">https://doi.org/10.1145/3808296</a>.","mla":"Chatterjee, Krishnendu, et al. “SuperDP: Differential Privacy Refutation via Supermartingales.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, no. PLDI, 218, ACM, 2026, doi:<a href=\"https://doi.org/10.1145/3808296\">10.1145/3808296</a>.","ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218.","short":"K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (2026)."},"publication_identifier":{"eissn":["2475-1421"]},"article_type":"original","date_published":"2026-06-08T00:00:00Z","department":[{"_id":"KrCh"}]}]