[{"publication_status":"published","PlanS_conform":"1","quality_controlled":"1","corr_author":"1","researchdata_availability":"yes","oa":1,"file_date_updated":"2026-06-24T06:19:56Z","publisher":"Association for Computing Machinery","ddc":["000"],"has_accepted_license":"1","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu"},{"orcid":"0000-0002-8595-0587","last_name":"Kafshdar Goharshadi","full_name":"Kafshdar Goharshadi, Ehsan","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde"}],"_id":"22102","date_updated":"2026-06-24T06:39:37Z","external_id":{"arxiv":["2603.26215"]},"day":"08","OA_type":"gold","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"status":"public","related_material":{"record":[{"status":"public","id":"22134","relation":"research_data"}]},"department":[{"_id":"KrCh"}],"month":"06","volume":10,"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."}],"article_processing_charge":"Yes","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"ec_funded":1,"article_type":"original","date_created":"2026-06-21T22:02:59Z","citation":{"short":"K. Chatterjee, E. Goharshady, D. Zikelic, Proceedings of the ACM on Programming Languages 10 (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>","ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218.","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. Association for Computing Machinery, 2026.","chicago":"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>.","apa":"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>","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, Association for Computing Machinery, 2026, doi:<a href=\"https://doi.org/10.1145/3808296\">10.1145/3808296</a>."},"supplementarymaterial":"no","OA_place":"publisher","file":[{"success":1,"checksum":"994bf21d6269dabccf1e1091e02962c5","content_type":"application/pdf","file_size":858595,"file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","date_updated":"2026-06-24T06:19:56Z","access_level":"open_access","creator":"dernst","date_created":"2026-06-24T06:19:56Z","relation":"main_file","file_id":"22135"}],"oa_version":"Published Version","das_tickbox":"1","doi":"10.1145/3808296","type":"journal_article","date_published":"2026-06-08T00:00:00Z","publication":"Proceedings of the ACM on Programming Languages","language":[{"iso":"eng"}],"scopus_import":"1","intvolume":"        10","year":"2026","issue":"PLDI","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.","arxiv":1,"publication_identifier":{"eissn":["2475-1421"]},"article_number":"218","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.","title":"SuperDP: Differential privacy refutation via supermartingales"},{"publication_status":"published","quality_controlled":"1","file_date_updated":"2020-07-14T12:47:20Z","oa":1,"conference":{"start_date":"2019-06-22","name":"PLDI: Conference on Programming Language Design and Implementation","end_date":"2019-06-26","location":"Phoenix, AZ, United States"},"author":[{"last_name":"Wang","full_name":"Wang, Peixin","first_name":"Peixin"},{"first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","last_name":"Fu","full_name":"Fu, Hongfei"},{"last_name":"Goharshady","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87","first_name":"Amir Kafshdar"},{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X"},{"last_name":"Qin","full_name":"Qin, Xudong","first_name":"Xudong"},{"last_name":"Shi","full_name":"Shi, Wenjun","first_name":"Wenjun"}],"_id":"6175","has_accepted_license":"1","ddc":["000"],"publisher":"Association for Computing Machinery","date_updated":"2026-06-26T22:34:23Z","page":"204-220","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","external_id":{"arxiv":["1902.04659"],"isi":["000523190300014"]},"day":"08","keyword":["Program Cost Analysis","Program Termination","Probabilistic Programs","Martingales"],"project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003"},{"call_identifier":"FWF","grant_number":"S11407","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"_id":"266EEEC0-B435-11E9-9278-68D0E5697425","name":"Quantitative Game-theoretic Analysis of Blockchain Applications and Smart Contracts"}],"related_material":{"record":[{"relation":"earlier_version","id":"5457","status":"public"},{"relation":"dissertation_contains","status":"public","id":"8934"}]},"status":"public","article_processing_charge":"No","month":"06","abstract":[{"text":"We consider the problem of expected cost analysis over nondeterministic probabilistic programs,\r\nwhich aims at automated methods for analyzing the resource-usage of such programs.\r\nPrevious approaches for this problem could only handle nonnegative bounded costs.\r\nHowever, in many scenarios, such as queuing networks or analysis of cryptocurrency protocols,\r\nboth positive and negative costs are necessary and the costs are unbounded as well.\r\n\r\nIn this work, we present a sound and efficient approach to obtain polynomial bounds on the\r\nexpected accumulated cost of nondeterministic probabilistic programs.\r\nOur approach can handle (a) general positive and negative costs with bounded updates in\r\nvariables; and (b) nonnegative costs with general updates to variables.\r\nWe show that several natural examples which could not be\r\nhandled by previous approaches are captured in our framework.\r\n\r\nMoreover, our approach leads to an efficient polynomial-time algorithm, while no\r\nprevious approach for cost analysis of probabilistic programs could guarantee polynomial runtime.\r\nFinally, we show the effectiveness of our approach using experimental results on a variety of programs for which we efficiently synthesize tight resource-usage bounds.","lang":"eng"}],"isi":1,"department":[{"_id":"KrCh"}],"date_created":"2019-03-25T10:13:25Z","ec_funded":1,"oa_version":"Submitted Version","file":[{"relation":"main_file","creator":"akafshda","date_created":"2019-03-25T10:11:22Z","file_id":"6176","access_level":"open_access","date_updated":"2020-07-14T12:47:20Z","file_size":4051066,"file_name":"paper.pdf","content_type":"application/pdf","checksum":"703a5e9b8c8587f2a44085ffd9a4db64"}],"citation":{"ista":"Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. 2019. Cost analysis of nondeterministic probabilistic programs. PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI: Conference on Programming Language Design and Implementation, 204–220.","ieee":"P. Wang, H. Fu, A. K. Goharshady, K. Chatterjee, X. Qin, and W. Shi, “Cost analysis of nondeterministic probabilistic programs,” in <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Phoenix, AZ, United States, 2019, pp. 204–220.","chicago":"Wang, Peixin, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. “Cost Analysis of Nondeterministic Probabilistic Programs.” In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, 204–20. Association for Computing Machinery, 2019. <a href=\"https://doi.org/10.1145/3314221.3314581\">https://doi.org/10.1145/3314221.3314581</a>.","apa":"Wang, P., Fu, H., Goharshady, A. K., Chatterjee, K., Qin, X., &#38; Shi, W. (2019). Cost analysis of nondeterministic probabilistic programs. In <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i> (pp. 204–220). Phoenix, AZ, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3314221.3314581\">https://doi.org/10.1145/3314221.3314581</a>","mla":"Wang, Peixin, et al. “Cost Analysis of Nondeterministic Probabilistic Programs.” <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2019, pp. 204–20, doi:<a href=\"https://doi.org/10.1145/3314221.3314581\">10.1145/3314221.3314581</a>.","short":"P. Wang, H. Fu, A.K. Goharshady, K. Chatterjee, X. Qin, W. Shi, in:, PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2019, pp. 204–220.","ama":"Wang P, Fu H, Goharshady AK, Chatterjee K, Qin X, Shi W. Cost analysis of nondeterministic probabilistic programs. In: <i>PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2019:204-220. doi:<a href=\"https://doi.org/10.1145/3314221.3314581\">10.1145/3314221.3314581</a>"},"doi":"10.1145/3314221.3314581","scopus_import":"1","language":[{"iso":"eng"}],"publication":"PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","date_published":"2019-06-08T00:00:00Z","type":"conference","year":"2019","title":"Cost analysis of nondeterministic probabilistic programs","arxiv":1}]