[{"issue":"PLDI","file_date_updated":"2026-06-24T06:19:56Z","month":"06","article_processing_charge":"Yes","volume":10,"language":[{"iso":"eng"}],"ddc":["000"],"year":"2026","quality_controlled":"1","PlanS_conform":"1","intvolume":"        10","has_accepted_license":"1","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.","publisher":"Association for Computing Machinery","corr_author":"1","type":"journal_article","publication_status":"published","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."}],"citation":{"ista":"Chatterjee K, Goharshady E, Zikelic D. 2026. SuperDP: Differential privacy refutation via supermartingales. Proceedings of the ACM on Programming Languages. 10(PLDI), 218.","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>.","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.","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>","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>."},"related_material":{"record":[{"status":"public","id":"22134","relation":"research_data"}]},"doi":"10.1145/3808296","scopus_import":"1","department":[{"_id":"KrCh"}],"day":"08","das_tickbox":"1","ec_funded":1,"OA_place":"publisher","article_type":"original","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.","title":"SuperDP: Differential privacy refutation via supermartingales","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"tmp":{"short":"CC BY (4.0)","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)"},"date_updated":"2026-06-24T06:39:37Z","keyword":["Static Program Analysis","Differential Privacy","Probabilistic Programming","Martingales"],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"22135","access_level":"open_access","content_type":"application/pdf","success":1,"date_updated":"2026-06-24T06:19:56Z","file_size":858595,"checksum":"994bf21d6269dabccf1e1091e02962c5","date_created":"2026-06-24T06:19:56Z","relation":"main_file","file_name":"2026_ProcACMProgrammingLanguages_Chatterjee.pdf","creator":"dernst"}],"publication":"Proceedings of the ACM on Programming Languages","project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"_id":"22102","article_number":"218","oa_version":"Published Version","date_created":"2026-06-21T22:02:59Z","external_id":{"arxiv":["2603.26215"]},"researchdata_availability":"yes","oa":1,"publication_identifier":{"eissn":["2475-1421"]},"OA_type":"gold","arxiv":1,"date_published":"2026-06-08T00:00:00Z"},{"scopus_import":"1","doi":"10.1145/3776682","citation":{"apa":"Mück, N., Georges, A. L., Dreyer, D., Garg, D., &#38; Sammler, M. J. (2026). Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3776682\">https://doi.org/10.1145/3776682</a>","mla":"Mück, Niklas, et al. “Endangered by the Language but Saved by the Compiler: Robust Safety via Semantic Back-Translation.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10, Association for Computing Machinery, 2026, pp. 1153–82, doi:<a href=\"https://doi.org/10.1145/3776682\">10.1145/3776682</a>.","ama":"Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. <i>Proceedings of the ACM on Programming Languages</i>. 2026;10:1153-1182. doi:<a href=\"https://doi.org/10.1145/3776682\">10.1145/3776682</a>","short":"N. Mück, A.L. Georges, D. Dreyer, D. Garg, M.J. Sammler, Proceedings of the ACM on Programming Languages 10 (2026) 1153–1182.","chicago":"Mück, Niklas, Aïna Linn Georges, Derek Dreyer, Deepak Garg, and Michael Joachim Sammler. “Endangered by the Language but Saved by the Compiler: Robust Safety via Semantic Back-Translation.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3776682\">https://doi.org/10.1145/3776682</a>.","ieee":"N. Mück, A. L. Georges, D. Dreyer, D. Garg, and M. J. Sammler, “Endangered by the language but saved by the compiler: Robust safety via semantic back-translation,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 10. Association for Computing Machinery, pp. 1153–1182, 2026.","ista":"Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. 2026. Endangered by the language but saved by the compiler: Robust safety via semantic back-translation. Proceedings of the ACM on Programming Languages. 10, 1153–1182."},"abstract":[{"text":"It is common for programmers to assemble their programs from a combination of trusted and untrusted components. In this context, a trusted program component is said to be robustly safe if it behaves safely when linked against arbitrary untrusted code. Prior work has shown how various encapsulation mechanisms (in both high- and low-level languages) can be used to protect code so that it is robustly safe, but none of the existing work has explored how robust safety can be achieved in a patently unsafe language like C.\r\nIn this paper, we show how to bring robust safety to a simple yet representative C-like language we call Rec. Although Rec (like C) is inherently ”dangerous” and thus not robustly safe, we can ”save” Rec programs via compilation to Cap, a CHERI-like capability machine. To formalize the benefits of such a hardening compiler, we develop Reckon, a separation logic for verifying robust safety of Rec programs. Reckon is not sound under Rec’s unsafe, C-like semantics, but it is sound when Rec programs are hardened via compilation and linked against untrusted code running on Cap. As a crucial step in proving soundness of Reckon, we introduce a novel technique of semantic back-translation, which we formalize by building on the DimSum framework for multi-language semantics. All our results are mechanized in the Rocq prover.","lang":"eng"}],"publication_status":"published","publisher":"Association for Computing Machinery","type":"journal_article","has_accepted_license":"1","PlanS_conform":"1","intvolume":"        10","quality_controlled":"1","year":"2026","ddc":["000"],"language":[{"iso":"eng"}],"volume":10,"article_processing_charge":"Yes (via OA deal)","month":"01","file_date_updated":"2026-02-12T13:51:03Z","page":"1153-1182","date_published":"2026-01-08T00:00:00Z","OA_type":"hybrid","publication_identifier":{"eissn":["2475-1421"]},"oa":1,"date_created":"2026-01-25T23:01:40Z","oa_version":"Published Version","_id":"21041","publication":"Proceedings of the ACM on Programming Languages","file":[{"file_id":"21221","access_level":"open_access","success":1,"content_type":"application/pdf","date_updated":"2026-02-12T13:51:03Z","file_size":1058876,"checksum":"79be391061efbf9542638996959ce11a","date_created":"2026-02-12T13:51:03Z","relation":"main_file","file_name":"2026_ProcACMProgrammingLanguages_Mueck.pdf","creator":"dernst"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_updated":"2026-02-12T13:53:04Z","tmp":{"short":"CC BY (4.0)","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)"},"author":[{"first_name":"Niklas","last_name":"Mück","full_name":"Mück, Niklas"},{"full_name":"Georges, Aïna Linn","first_name":"Aïna Linn","last_name":"Georges"},{"full_name":"Dreyer, Derek","first_name":"Derek","last_name":"Dreyer"},{"full_name":"Garg, Deepak","last_name":"Garg","first_name":"Deepak"},{"last_name":"Sammler","first_name":"Michael Joachim","full_name":"Sammler, Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"}],"title":"Endangered by the language but saved by the compiler: Robust safety via semantic back-translation","OA_place":"publisher","article_type":"original","day":"08","department":[{"_id":"MiSa"}]},{"article_processing_charge":"Yes (in subscription journal)","file_date_updated":"2025-06-30T09:01:08Z","page":"848-873","issue":"PLDI","month":"06","year":"2025","ddc":["000"],"quality_controlled":"1","volume":9,"language":[{"iso":"eng"}],"type":"journal_article","corr_author":"1","publisher":"Association for Computing Machinery","publication_status":"published","intvolume":"         9","has_accepted_license":"1","doi":"10.1145/3729284","scopus_import":"1","abstract":[{"text":"The separation logic framework Iris has been built on the premise that all assertions are stable, meaning they unconditionally enjoy the famous frame rule. This gives Iris—and the numerous program logics that build on it—very modular reasoning principles. But stability also comes at a cost. It excludes a core feature of the Viper verifier family, heap-dependent expression assertions, which lift program expressions to the assertion level in order to reduce redundancy between code and specifications and better facilitate SMT-based automation.\r\nIn this paper, we bring heap-dependent expression assertions to Iris with Daenerys. To do so, we must first revisit the very core of Iris, extending it with a new form of unstable resources (and adapting the frame rule accordingly). On top, we then build a program logic with heap-dependent expression assertions and lay the foundations for connecting Iris to SMT solvers. We apply Daenerys to several case studies, including some that go beyond what Viper and Iris can do individually and others that benefit from the connection to SMT.","lang":"eng"}],"citation":{"ieee":"S. Spies <i>et al.</i>, “Destabilizing Iris,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. PLDI. Association for Computing Machinery, pp. 848–873, 2025.","chicago":"Spies, Simon, Niklas Mück, Haoyi Zeng, Michael Joachim Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer. “Destabilizing Iris.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3729284\">https://doi.org/10.1145/3729284</a>.","ista":"Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025. Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI), 848–873.","ama":"Spies S, Mück N, Zeng H, et al. Destabilizing Iris. <i>Proceedings of the ACM on Programming Languages</i>. 2025;9(PLDI):848-873. doi:<a href=\"https://doi.org/10.1145/3729284\">10.1145/3729284</a>","short":"S. Spies, N. Mück, H. Zeng, M.J. Sammler, A. Lattuada, P. Müller, D. Dreyer, Proceedings of the ACM on Programming Languages 9 (2025) 848–873.","apa":"Spies, S., Mück, N., Zeng, H., Sammler, M. J., Lattuada, A., Müller, P., &#38; Dreyer, D. (2025). Destabilizing Iris. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3729284\">https://doi.org/10.1145/3729284</a>","mla":"Spies, Simon, et al. “Destabilizing Iris.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp. 848–73, doi:<a href=\"https://doi.org/10.1145/3729284\">10.1145/3729284</a>."},"title":"Destabilizing Iris","author":[{"full_name":"Spies, Simon","first_name":"Simon","last_name":"Spies"},{"full_name":"Mück, Niklas","first_name":"Niklas","last_name":"Mück"},{"full_name":"Zeng, Haoyi","last_name":"Zeng","first_name":"Haoyi"},{"full_name":"Sammler, Michael Joachim","last_name":"Sammler","first_name":"Michael Joachim","id":"510d3901-2a03-11ee-914d-d9ae9011f0a7"},{"full_name":"Lattuada, Andrea","last_name":"Lattuada","first_name":"Andrea"},{"last_name":"Müller","first_name":"Peter","full_name":"Müller, Peter"},{"first_name":"Derek","last_name":"Dreyer","full_name":"Dreyer, Derek"}],"department":[{"_id":"MiSa"}],"day":"01","acknowledgement":"We would like to thank the anonymous reviewers for their helpful feedback and Alex Summers\r\nfor insightful discussions. This work was funded in part by a Google PhD Fellowship for the first\r\nauthor.","article_type":"original","OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-06-30T09:10:11Z","tmp":{"short":"CC BY (4.0)","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)"},"status":"public","_id":"19935","date_created":"2025-06-30T08:47:31Z","oa_version":"Published Version","file":[{"access_level":"open_access","date_updated":"2025-06-30T09:01:08Z","success":1,"content_type":"application/pdf","file_id":"19938","file_name":"2025_ProcACMProg_Spies.pdf","creator":"dernst","date_created":"2025-06-30T09:01:08Z","checksum":"6b72d84c10a10ba7cd1646e2c36dc1ff","file_size":843343,"relation":"main_file"}],"publication":"Proceedings of the ACM on Programming Languages","publication_identifier":{"eissn":["2475-1421"]},"OA_type":"hybrid","date_published":"2025-06-01T00:00:00Z","oa":1},{"title":"Quantitative bounds on resource usage of probabilistic programs","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu"},{"last_name":"Goharshady","first_name":"Amir Kafshdar","orcid":"0000-0003-1702-6584","full_name":"Goharshady, Amir Kafshdar","id":"391365CE-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165","first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"acknowledgement":"This work was supported in part by the European Research Council (ERC) under Grant No. 863818\r\n(ForM-SMArt) and the Hong Kong Research Grants Council under ECS Project No. 26208122.","article_type":"original","ec_funded":1,"department":[{"_id":"KrCh"}],"day":"29","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_updated":"2025-04-14T07:52:47Z","tmp":{"short":"CC BY (4.0)","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)"},"date_created":"2024-06-23T22:01:02Z","article_number":"107","oa_version":"Published Version","_id":"17162","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"}],"publication":"Proceedings of the ACM on Programming Languages","file":[{"relation":"main_file","checksum":"9243ded966f71df1572be5466019be5c","date_created":"2024-06-27T07:48:16Z","file_size":413096,"creator":"dernst","file_name":"2024_ProcACMProgLanguage_Chatterjee.pdf","file_id":"17182","date_updated":"2024-06-27T07:48:16Z","content_type":"application/pdf","success":1,"access_level":"open_access"}],"date_published":"2024-04-29T00:00:00Z","publication_identifier":{"eissn":["2475-1421"]},"oa":1,"article_processing_charge":"Yes (in subscription journal)","month":"04","file_date_updated":"2024-06-27T07:48:16Z","issue":"OOPSLA1","quality_controlled":"1","ddc":["000"],"year":"2024","language":[{"iso":"eng"}],"volume":8,"publication_status":"published","publisher":"Association for Computing Machinery","type":"journal_article","has_accepted_license":"1","intvolume":"         8","scopus_import":"1","doi":"10.1145/3649824","citation":{"ieee":"K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and D. Zikelic, “Quantitative bounds on resource usage of probabilistic programs,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, no. OOPSLA1. Association for Computing Machinery, 2024.","ista":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. 2024. Quantitative bounds on resource usage of probabilistic programs. Proceedings of the ACM on Programming Languages. 8(OOPSLA1), 107.","chicago":"Chatterjee, Krishnendu, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. “Quantitative Bounds on Resource Usage of Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3649824\">https://doi.org/10.1145/3649824</a>.","ama":"Chatterjee K, Goharshady AK, Meggendorfer T, Zikelic D. Quantitative bounds on resource usage of probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. 2024;8(OOPSLA1). doi:<a href=\"https://doi.org/10.1145/3649824\">10.1145/3649824</a>","short":"K. Chatterjee, A.K. Goharshady, T. Meggendorfer, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","apa":"Chatterjee, K., Goharshady, A. K., Meggendorfer, T., &#38; Zikelic, D. (2024). Quantitative bounds on resource usage of probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3649824\">https://doi.org/10.1145/3649824</a>","mla":"Chatterjee, Krishnendu, et al. “Quantitative Bounds on Resource Usage of Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, no. OOPSLA1, 107, Association for Computing Machinery, 2024, doi:<a href=\"https://doi.org/10.1145/3649824\">10.1145/3649824</a>."},"abstract":[{"text":"Cost analysis, also known as resource usage analysis, is the task of finding bounds on the total cost of a program and is a well-studied problem in static analysis. In this work, we consider two classical quantitative problems in cost analysis for probabilistic programs. The first problem is to find a bound on the expected total cost of the program. This is a natural measure for the resource usage of the program and can also be directly applied to average-case runtime analysis. The second problem asks for a tail bound, i.e. ‍given a threshold t the goal is to find a probability bound p such that ℙ[total cost ≥ t] ≤ p. Intuitively, given a threshold t on the resource, the problem is to find the likelihood that the total cost exceeds this threshold.\r\nFirst, for expectation bounds, a major obstacle in previous works on cost analysis is that they can handle only non-negative costs or bounded variable updates. In contrast, we provide a new variant of the standard notion of cost martingales, that allows us to find expectation bounds for a class of programs with general positive or negative costs and no restriction on the variable updates. More specifically, our approach is applicable as long as there is a lower bound on the total cost incurred along every path.\r\nSecond, for tail bounds, all previous methods are limited to programs in which the expected total cost is finite. In contrast, we present a novel approach, based on a combination of our martingale-based method for expectation bounds with a quantitative safety analysis, to obtain a solution to the tail bound problem that is applicable even to programs with infinite expected cost. Specifically, this allows us to obtain runtime tail bounds for programs that do not terminate almost-surely.\r\nIn summary, we provide a novel combination of martingale-based cost analysis and quantitative safety analysis that is able to find expectation and tail cost bounds for probabilistic programs, without the restrictions of non-negative costs, bounded updates, or finiteness of the expected total cost. Finally, we provide experimental results showcasing that our approach can solve instances that were beyond the reach of previous methods.","lang":"eng"}]},{"intvolume":"         8","has_accepted_license":"1","publisher":"Association for Computing Machinery","type":"journal_article","corr_author":"1","publication_status":"published","abstract":[{"text":"We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.","lang":"eng"}],"citation":{"chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Equivalence and Similarity Refutation for Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3656462\">https://doi.org/10.1145/3656462</a>.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Equivalence and similarity refutation for probabilistic programs,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8. Association for Computing Machinery, 2024.","ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 8, 232.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Equivalence and similarity refutation for probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. 2024;8. doi:<a href=\"https://doi.org/10.1145/3656462\">10.1145/3656462</a>","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","mla":"Chatterjee, Krishnendu, et al. “Equivalence and Similarity Refutation for Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, 232, Association for Computing Machinery, 2024, doi:<a href=\"https://doi.org/10.1145/3656462\">10.1145/3656462</a>.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2024). Equivalence and similarity refutation for probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3656462\">https://doi.org/10.1145/3656462</a>"},"doi":"10.1145/3656462","scopus_import":"1","file_date_updated":"2024-07-22T07:17:14Z","month":"06","article_processing_charge":"Yes (via OA deal)","volume":8,"language":[{"iso":"eng"}],"year":"2024","ddc":["000"],"quality_controlled":"1","file":[{"access_level":"open_access","content_type":"application/pdf","success":1,"date_updated":"2024-07-22T07:17:14Z","file_id":"17290","file_name":"2024_ACMProgLang_Chatterjee.pdf","creator":"dernst","file_size":355421,"checksum":"8cbf220f284a4a87d093db5320c5afdd","date_created":"2024-07-22T07:17:14Z","relation":"main_file"}],"publication":"Proceedings of the ACM on Programming Languages","_id":"17283","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"date_created":"2024-07-21T22:01:01Z","oa_version":"Published Version","article_number":"232","oa":1,"external_id":{"arxiv":["2404.03430"]},"arxiv":1,"publication_identifier":{"eissn":["2475-1421"]},"OA_type":"hybrid","date_published":"2024-06-20T00:00:00Z","ec_funded":1,"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"day":"20","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant. Petr Novotný\r\nis supported by the Czech Science Foundation grant no. GA23-06963S.\r\n","article_type":"original","OA_place":"publisher","title":"Equivalence and similarity refutation for probabilistic programs","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","first_name":"Petr","last_name":"Novotný"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"date_updated":"2025-04-14T07:52:47Z","tmp":{"short":"CC BY (4.0)","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)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87"},{"volume":7,"language":[{"iso":"eng"}],"year":"2023","ddc":["000"],"quality_controlled":"1","file_date_updated":"2023-07-03T13:09:39Z","month":"06","article_processing_charge":"No","abstract":[{"lang":"eng","text":"Writing concurrent code that is both correct and efficient is notoriously difficult. Thus, programmers often prefer to use synchronization abstractions, which render code simpler and easier to reason about. Despite a wealth of work on this topic, there is still a gap between the rich semantics provided by synchronization abstractions in modern programming languages—specifically, fair FIFO ordering of synchronization requests and support for abortable operations—and frameworks for implementing it correctly and efficiently. Supporting such semantics is critical given the rising popularity of constructs for asynchronous programming, such as coroutines, which abort frequently and are cheaper to suspend and resume compared to native threads.\r\n\r\nThis paper introduces a new framework called CancellableQueueSynchronizer (CQS), which enables simple yet efficient implementations of a wide range of fair and abortable synchronization primitives: mutexes, semaphores, barriers, count-down latches, and blocking pools. Our main contribution is algorithmic, as implementing both fairness and abortability efficiently at this level of generality is non-trivial. Importantly, all our algorithms, including the CQS framework and the primitives built on top of it, come with formal proofs in the Iris framework for Coq for many of their properties. These proofs are modular, so it is easy to show correctness for new primitives implemented on top of CQS. From a practical perspective, implementation of CQS for native threads on the JVM improves throughput by up to two orders of magnitude over Java’s AbstractQueuedSynchronizer, the only practical abstraction offering similar semantics. Further, we successfully integrated CQS as a core component of the popular Kotlin Coroutines library, validating the framework’s practical impact and expressiveness in a real-world environment. In sum, CancellableQueueSynchronizer is the first framework to combine expressiveness with formal guarantees and solid practical performance. Our approach should be extensible to other languages and families of synchronization primitives."}],"citation":{"ieee":"N. Koval, D. Khalanskiy, and D.-A. Alistarh, “CQS: A formally-verified framework for fair and abortable synchronization,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7. Association for Computing Machinery, 2023.","chicago":"Koval, Nikita, Dmitry Khalanskiy, and Dan-Adrian Alistarh. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3591230\">https://doi.org/10.1145/3591230</a>.","ista":"Koval N, Khalanskiy D, Alistarh D-A. 2023. CQS: A formally-verified framework for fair and abortable synchronization. Proceedings of the ACM on Programming Languages. 7, 116.","short":"N. Koval, D. Khalanskiy, D.-A. Alistarh, Proceedings of the ACM on Programming Languages 7 (2023).","ama":"Koval N, Khalanskiy D, Alistarh D-A. CQS: A formally-verified framework for fair and abortable synchronization. <i>Proceedings of the ACM on Programming Languages</i>. 2023;7. doi:<a href=\"https://doi.org/10.1145/3591230\">10.1145/3591230</a>","mla":"Koval, Nikita, et al. “CQS: A Formally-Verified Framework for Fair and Abortable Synchronization.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 7, 116, Association for Computing Machinery, 2023, doi:<a href=\"https://doi.org/10.1145/3591230\">10.1145/3591230</a>.","apa":"Koval, N., Khalanskiy, D., &#38; Alistarh, D.-A. (2023). CQS: A formally-verified framework for fair and abortable synchronization. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3591230\">https://doi.org/10.1145/3591230</a>"},"doi":"10.1145/3591230","scopus_import":"1","intvolume":"         7","has_accepted_license":"1","type":"journal_article","corr_author":"1","publisher":"Association for Computing Machinery","publication_status":"published","tmp":{"short":"CC BY (4.0)","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)"},"date_updated":"2026-07-06T12:12:08Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","department":[{"_id":"DaAl"}],"day":"06","das_tickbox":"1","article_type":"original","title":"CQS: A formally-verified framework for fair and abortable synchronization","author":[{"id":"2F4DB10C-F248-11E8-B48F-1D18A9856A87","first_name":"Nikita","last_name":"Koval","full_name":"Koval, Nikita"},{"full_name":"Khalanskiy, Dmitry","first_name":"Dmitry","last_name":"Khalanskiy"},{"id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","last_name":"Alistarh","first_name":"Dan-Adrian","orcid":"0000-0003-3650-940X","full_name":"Alistarh, Dan-Adrian"}],"oa":1,"publication_identifier":{"eissn":["2475-1421"]},"date_published":"2023-06-06T00:00:00Z","file":[{"file_id":"13187","content_type":"application/pdf","success":1,"date_updated":"2023-07-03T13:09:39Z","access_level":"open_access","relation":"main_file","file_size":1266773,"checksum":"5dba6e73f0ed79adbdae14d165bc2f68","date_created":"2023-07-03T13:09:39Z","creator":"alisjak","file_name":"2023_ACMProgram.Lang._Koval.pdf"}],"publication":"Proceedings of the ACM on Programming Languages","_id":"13179","oa_version":"Published Version","article_number":"116","date_created":"2023-07-02T22:00:43Z"},{"volume":5,"language":[{"iso":"eng"}],"year":"2021","conference":{"name":"OOPSLA: Object-Oriented Programming, Systems, Languages, and Applications","end_date":"2021-10-23","location":"Chicago, IL, United States","start_date":"2021-10-17"},"ddc":["005"],"quality_controlled":"1","file_date_updated":"2021-10-19T12:52:23Z","month":"10","article_processing_charge":"No","abstract":[{"lang":"eng","text":"Gradual typing is a principled means for mixing typed and untyped code. But typed and untyped code often exhibit different programming patterns. There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns. This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well.\r\n\r\nIn particular, we explore mixing untyped \"structural\" code with typed \"nominal\" code in an object-oriented language. But whereas previous work only allowed \"nominal\" objects to be treated as \"structural\" objects, we also allow \"structural\" objects to dynamically acquire certain nominal types, namely interfaces. We present a calculus that supports such \"cross-paradigm\" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently."}],"citation":{"apa":"Mühlböck, F., &#38; Tate, R. (2021). Transitioning from structural to nominal code with efficient gradual typing. <i>Proceedings of the ACM on Programming Languages</i>. Chicago, IL, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3485504\">https://doi.org/10.1145/3485504</a>","mla":"Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal Code with Efficient Gradual Typing.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5, 127, Association for Computing Machinery, 2021, doi:<a href=\"https://doi.org/10.1145/3485504\">10.1145/3485504</a>.","ama":"Mühlböck F, Tate R. Transitioning from structural to nominal code with efficient gradual typing. <i>Proceedings of the ACM on Programming Languages</i>. 2021;5. doi:<a href=\"https://doi.org/10.1145/3485504\">10.1145/3485504</a>","short":"F. Mühlböck, R. Tate, Proceedings of the ACM on Programming Languages 5 (2021).","chicago":"Mühlböck, Fabian, and Ross Tate. “Transitioning from Structural to Nominal Code with Efficient Gradual Typing.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3485504\">https://doi.org/10.1145/3485504</a>.","ista":"Mühlböck F, Tate R. 2021. Transitioning from structural to nominal code with efficient gradual typing. Proceedings of the ACM on Programming Languages. 5, 127.","ieee":"F. Mühlböck and R. Tate, “Transitioning from structural to nominal code with efficient gradual typing,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5. Association for Computing Machinery, 2021."},"doi":"10.1145/3485504","scopus_import":"1","intvolume":"         5","has_accepted_license":"1","publisher":"Association for Computing Machinery","type":"journal_article","publication_status":"published","tmp":{"short":"CC BY-ND (4.0)","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode"},"keyword":["gradual typing","gradual guarantee","nominal","structural","call tags"],"date_updated":"2025-04-15T06:25:55Z","status":"public","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","day":"15","department":[{"_id":"ToHe"}],"article_type":"original","acknowledgement":"We thank the reviewers for their valuable suggestions towards improving the paper. We also \r\nthank Mae Milano and Adrian Sampson, as well as the members of the Programming Languages Discussion Group at Cornell University and of the Programming Research Laboratory at Northeastern University, for their helpful feedback on preliminary findings of this work.\r\n\r\nThis material is based upon work supported in part by the National Science Foundation (NSF) through grant CCF-1350182 and the Austrian Science Fund (FWF) through grant Z211-N23 (Wittgenstein~Award).\r\nAny opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the NSF or the FWF.","author":[{"id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian","last_name":"Mühlböck","full_name":"Mühlböck, Fabian","orcid":"0000-0003-1548-0177"},{"full_name":"Tate, Ross","first_name":"Ross","last_name":"Tate"}],"title":"Transitioning from structural to nominal code with efficient gradual typing","oa":1,"publication_identifier":{"eissn":["2475-1421"]},"date_published":"2021-10-15T00:00:00Z","file":[{"file_name":"monnom-oopsla21.pdf","creator":"fmuehlbo","date_created":"2021-10-19T12:52:23Z","checksum":"71011efd2da771cafdec7f0d9693f8c1","file_size":770269,"relation":"main_file","access_level":"open_access","date_updated":"2021-10-19T12:52:23Z","success":1,"content_type":"application/pdf","file_id":"10154"}],"publication":"Proceedings of the ACM on Programming Languages","project":[{"call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"_id":"10153","oa_version":"Published Version","article_number":"127","date_created":"2021-10-19T12:48:44Z"},{"type":"journal_article","publisher":"Association for Computing Machinery","publication_status":"published","intvolume":"         5","has_accepted_license":"1","related_material":{"record":[{"id":"10199","relation":"dissertation_contains","status":"public"}]},"doi":"10.1145/3485541","scopus_import":"1","abstract":[{"text":"In this work we solve the algorithmic problem of consistency verification for the TSO and PSO memory models given a reads-from map, denoted VTSO-rf and VPSO-rf, respectively. For an execution of n events over k threads and d variables, we establish novel bounds that scale as nk+1 for TSO and as nk+1· min(nk2, 2k· d) for PSO. Moreover, based on our solution to these problems, we develop an SMC algorithm under TSO and PSO that uses the RF equivalence. The algorithm is exploration-optimal, in the sense that it is guaranteed to explore each class of the RF partitioning exactly once, and spends polynomial time per class when k is bounded. Finally, we implement all our algorithms in the SMC tool Nidhugg, and perform a large number of experiments over benchmarks from existing literature. Our experimental results show that our algorithms for VTSO-rf and VPSO-rf provide significant scalability improvements over standard alternatives. Moreover, when used for SMC, the RF partitioning is often much coarser than the standard Shasha-Snir partitioning for TSO/PSO, which yields a significant speedup in the model checking task.\r\n\r\n","lang":"eng"}],"citation":{"apa":"Bui, T. L., Chatterjee, K., Gautam, T., Pavlogiannis, A., &#38; Toman, V. (2021). The reads-from equivalence for the TSO and PSO memory models. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3485541\">https://doi.org/10.1145/3485541</a>","mla":"Bui, Truc Lam, et al. “The Reads-from Equivalence for the TSO and PSO Memory Models.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5, no. OOPSLA, 164, Association for Computing Machinery, 2021, doi:<a href=\"https://doi.org/10.1145/3485541\">10.1145/3485541</a>.","short":"T.L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, V. Toman, Proceedings of the ACM on Programming Languages 5 (2021).","ama":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. The reads-from equivalence for the TSO and PSO memory models. <i>Proceedings of the ACM on Programming Languages</i>. 2021;5(OOPSLA). doi:<a href=\"https://doi.org/10.1145/3485541\">10.1145/3485541</a>","ieee":"T. L. Bui, K. Chatterjee, T. Gautam, A. Pavlogiannis, and V. Toman, “The reads-from equivalence for the TSO and PSO memory models,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 5, no. OOPSLA. Association for Computing Machinery, 2021.","ista":"Bui TL, Chatterjee K, Gautam T, Pavlogiannis A, Toman V. 2021. The reads-from equivalence for the TSO and PSO memory models. Proceedings of the ACM on Programming Languages. 5(OOPSLA), 164.","chicago":"Bui, Truc Lam, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman. “The Reads-from Equivalence for the TSO and PSO Memory Models.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3485541\">https://doi.org/10.1145/3485541</a>."},"article_processing_charge":"No","issue":"OOPSLA","file_date_updated":"2021-11-04T07:24:48Z","month":"10","year":"2021","ddc":["000"],"quality_controlled":"1","volume":5,"language":[{"iso":"eng"}],"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"}],"_id":"10191","oa_version":"Published Version","article_number":"164","date_created":"2021-10-27T15:05:34Z","file":[{"relation":"main_file","checksum":"9d6dce7b611853c529bb7b1915ac579e","date_created":"2021-11-04T07:24:48Z","file_size":2903485,"creator":"cchlebak","file_name":"2021_ProcACMPL_Bui.pdf","file_id":"10215","date_updated":"2021-11-04T07:24:48Z","success":1,"content_type":"application/pdf","access_level":"open_access"}],"publication":"Proceedings of the ACM on Programming Languages","publication_identifier":{"eissn":["2475-1421"]},"arxiv":1,"date_published":"2021-10-15T00:00:00Z","external_id":{"arxiv":["2011.11763"]},"oa":1,"author":[{"full_name":"Bui, Truc Lam","first_name":"Truc Lam","last_name":"Bui"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Gautam, Tushar","first_name":"Tushar","last_name":"Gautam"},{"last_name":"Pavlogiannis","first_name":"Andreas","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Viktor","last_name":"Toman","orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"title":"The reads-from equivalence for the TSO and PSO memory models","day":"15","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"ec_funded":1,"article_type":"original","acknowledgement":"The research was partially funded by the ERC CoG 863818 (ForM-SMArt) and the Vienna Science\r\nand Technology Fund (WWTF) through project ICT15-003.","user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","tmp":{"short":"CC BY (4.0)","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)"},"keyword":["safety","risk","reliability and quality","software"],"date_updated":"2026-04-08T07:00:31Z","status":"public"},{"external_id":{"arxiv":["1902.04744"]},"oa":1,"date_published":"2020-01-01T00:00:00Z","publication_identifier":{"eissn":["2475-1421"]},"arxiv":1,"publication":"Proceedings of the ACM on Programming Languages","file":[{"file_id":"8328","access_level":"open_access","date_updated":"2020-09-01T11:12:58Z","success":1,"content_type":"application/pdf","checksum":"c6193d109ff4ecb17e7a6513d8eb34c0","date_created":"2020-09-01T11:12:58Z","file_size":564151,"relation":"main_file","file_name":"2019_ACM_POPL_Wang.pdf","creator":"cziletti"}],"oa_version":"Published Version","article_number":"25","date_created":"2020-08-30T22:01:12Z","project":[{"call_identifier":"FWF","name":"Game Theory","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"}],"_id":"8324","status":"public","tmp":{"short":"CC BY (4.0)","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)"},"date_updated":"2025-04-15T06:30:10Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","acknowledgement":"We thank anonymous reviewers for helpful comments, especially for pointing to us a scenario of piecewise-linear approximation (Remark5). The research was partially supported by the National Natural Science Foundation of China (NSFC) under Grant No. 61802254, 61672229, 61832015,61772336,11871221 and Austrian Science Fund (FWF) NFN under Grant No. S11407-N23 (RiSE/SHiNE). We thank Prof. Yuxi Fu, director of the BASICS Lab at Shanghai Jiao Tong University, for his support.","department":[{"_id":"KrCh"}],"day":"01","author":[{"first_name":"Peixin","last_name":"Wang","full_name":"Wang, Peixin"},{"full_name":"Fu, Hongfei","last_name":"Fu","first_name":"Hongfei"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Deng, Yuxin","first_name":"Yuxin","last_name":"Deng"},{"full_name":"Xu, Ming","last_name":"Xu","first_name":"Ming"}],"title":"Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time","citation":{"mla":"Wang, Peixin, et al. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 4, no. POPL, 25, ACM, 2020, doi:<a href=\"https://doi.org/10.1145/3371093\">10.1145/3371093</a>.","apa":"Wang, P., Fu, H., Chatterjee, K., Deng, Y., &#38; Xu, M. (2020). Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In <i>Proceedings of the ACM on Programming Languages</i> (Vol. 4). ACM. <a href=\"https://doi.org/10.1145/3371093\">https://doi.org/10.1145/3371093</a>","short":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM on Programming Languages, ACM, 2020.","ama":"Wang P, Fu H, Chatterjee K, Deng Y, Xu M. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In: <i>Proceedings of the ACM on Programming Languages</i>. Vol 4. ACM; 2020. doi:<a href=\"https://doi.org/10.1145/3371093\">10.1145/3371093</a>","ieee":"P. Wang, H. Fu, K. Chatterjee, Y. Deng, and M. Xu, “Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time,” in <i>Proceedings of the ACM on Programming Languages</i>, 2020, vol. 4, no. POPL.","chicago":"Wang, Peixin, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” In <i>Proceedings of the ACM on Programming Languages</i>, Vol. 4. ACM, 2020. <a href=\"https://doi.org/10.1145/3371093\">https://doi.org/10.1145/3371093</a>.","ista":"Wang P, Fu H, Chatterjee K, Deng Y, Xu M. 2020. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Proceedings of the ACM on Programming Languages. vol. 4, 25."},"abstract":[{"lang":"eng","text":"The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature."}],"scopus_import":"1","related_material":{"link":[{"url":"https://doi.org/10.5281/zenodo.3533633","relation":"software"}]},"doi":"10.1145/3371093","has_accepted_license":"1","intvolume":"         4","publication_status":"published","type":"conference","publisher":"ACM","language":[{"iso":"eng"}],"volume":4,"quality_controlled":"1","year":"2020","ddc":["004"],"month":"01","issue":"POPL","file_date_updated":"2020-09-01T11:12:58Z","article_processing_charge":"No"},{"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","tmp":{"short":"CC BY (4.0)","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)"},"date_updated":"2026-04-08T07:00:31Z","keyword":["safety","risk","reliability and quality","software"],"status":"public","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Pavlogiannis, Andreas","orcid":"0000-0002-8943-0722","last_name":"Pavlogiannis","first_name":"Andreas","id":"49704004-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-9036-063X","full_name":"Toman, Viktor","last_name":"Toman","first_name":"Viktor","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87"}],"title":"Value-centric dynamic partial order reduction","department":[{"_id":"GradSch"},{"_id":"KrCh"}],"day":"10","OA_place":"publisher","acknowledgement":"The authors would also like to thank anonymous referees for their valuable comments and helpful suggestions. This work is supported by the Austrian Science Fund (FWF) NFN grants S11407-N23 (RiSE/SHiNE) and S11402-N23 (RiSE/SHiNE), by the Vienna Science and Technology Fund (WWTF) Project ICT15-003, and by the Austrian Science Fund (FWF) Schrodinger grant J-4220.\r\n","publication_identifier":{"eissn":["2475-1421"]},"OA_type":"hybrid","arxiv":1,"date_published":"2019-10-10T00:00:00Z","external_id":{"arxiv":["1909.00989"]},"oa":1,"project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"name":"Game Theory","call_identifier":"FWF","grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"}],"_id":"10190","oa_version":"Published Version","article_number":"124","date_created":"2021-10-27T14:57:06Z","file":[{"creator":"cchlebak","file_name":"2019_ACM_Chatterjee.pdf","relation":"main_file","date_created":"2021-11-12T11:41:56Z","checksum":"2149979c46964c4d117af06ccb6c0834","file_size":570829,"date_updated":"2021-11-12T11:41:56Z","content_type":"application/pdf","success":1,"access_level":"open_access","file_id":"10278"}],"publication":"Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications","conference":{"start_date":"2019-10-23","name":"OOPSLA: Object-oriented Programming, Systems, Languages and Applications","end_date":"2019-10-25","location":"Athens, Greece"},"year":"2019","ddc":["000"],"quality_controlled":"1","volume":3,"language":[{"iso":"eng"}],"article_processing_charge":"No","file_date_updated":"2021-11-12T11:41:56Z","month":"10","related_material":{"record":[{"relation":"dissertation_contains","id":"10199","status":"public"}]},"doi":"10.1145/3360550","scopus_import":"1","abstract":[{"lang":"eng","text":"The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning."}],"citation":{"apa":"Chatterjee, K., Pavlogiannis, A., &#38; Toman, V. (2019). Value-centric dynamic partial order reduction. In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i> (Vol. 3). Athens, Greece: ACM. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>","mla":"Chatterjee, Krishnendu, et al. “Value-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, vol. 3, 124, ACM, 2019, doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>.","ista":"Chatterjee K, Pavlogiannis A, Toman V. 2019. Value-centric dynamic partial order reduction. Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications. OOPSLA: Object-oriented Programming, Systems, Languages and Applications vol. 3, 124.","chicago":"Chatterjee, Krishnendu, Andreas Pavlogiannis, and Viktor Toman. “Value-Centric Dynamic Partial Order Reduction.” In <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Vol. 3. ACM, 2019. <a href=\"https://doi.org/10.1145/3360550\">https://doi.org/10.1145/3360550</a>.","ieee":"K. Chatterjee, A. Pavlogiannis, and V. Toman, “Value-centric dynamic partial order reduction,” in <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>, Athens, Greece, 2019, vol. 3.","ama":"Chatterjee K, Pavlogiannis A, Toman V. Value-centric dynamic partial order reduction. In: <i>Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications</i>. Vol 3. ACM; 2019. doi:<a href=\"https://doi.org/10.1145/3360550\">10.1145/3360550</a>","short":"K. Chatterjee, A. Pavlogiannis, V. Toman, in:, Proceedings of the 34th ACM International Conference on Object-Oriented Programming, Systems, Languages, and Applications, ACM, 2019."},"corr_author":"1","publisher":"ACM","type":"conference","publication_status":"published","intvolume":"         3","has_accepted_license":"1"},{"ec_funded":1,"day":"01","department":[{"_id":"KrCh"}],"acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499- N23, FWF\r\nNFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), and Czech\r\nScience Foundation grant GBP202/12/G061.","article_type":"original","OA_place":"publisher","author":[{"full_name":"Chalupa, Marek","first_name":"Marek","last_name":"Chalupa"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"49704004-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas","last_name":"Pavlogiannis","orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas"},{"first_name":"Nishant","last_name":"Sinha","full_name":"Sinha, Nishant"},{"last_name":"Vaidya","first_name":"Kapil","full_name":"Vaidya, Kapil"}],"title":"Data-centric dynamic partial order reduction","date_updated":"2025-05-20T09:45:10Z","tmp":{"short":"CC BY (4.0)","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)"},"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"file_id":"19716","content_type":"application/pdf","success":1,"date_updated":"2025-05-20T09:44:47Z","access_level":"open_access","relation":"main_file","file_size":388891,"checksum":"b27ab1745f6dba2387deb785798a657c","date_created":"2025-05-20T09:44:47Z","creator":"dernst","file_name":"2018_ACM_Chalupa.pdf"}],"publication":"Proceedings of the ACM on Programming Languages","_id":"10417","project":[{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"}],"date_created":"2021-12-05T23:01:49Z","oa_version":"Published Version","article_number":"31","oa":1,"external_id":{"arxiv":["1610.01188"]},"arxiv":1,"publication_identifier":{"eissn":["2475-1421"]},"OA_type":"hybrid","date_published":"2018-01-01T00:00:00Z","file_date_updated":"2025-05-20T09:44:47Z","issue":"POPL","month":"01","article_processing_charge":"No","volume":2,"language":[{"iso":"eng"}],"ddc":["000"],"conference":{"start_date":"2018-01-07","name":"POPL: Programming Languages","end_date":"2018-01-13","location":"Los Angeles, CA, United States"},"year":"2018","quality_controlled":"1","intvolume":"         2","has_accepted_license":"1","publisher":"Association for Computing Machinery","type":"journal_article","publication_status":"published","abstract":[{"text":"We present a new dynamic partial-order reduction method for stateless model checking of concurrent programs. A common approach for exploring program behaviors relies on enumerating the traces of the program, without storing the visited states (aka stateless exploration). As the number of distinct traces grows exponentially, dynamic partial-order reduction (DPOR) techniques have been successfully used to partition the space of traces into equivalence classes (Mazurkiewicz partitioning), with the goal of exploring only few representative traces from each class.\r\n\r\nWe introduce a new equivalence on traces under sequential consistency semantics, which we call the observation equivalence. Two traces are observationally equivalent if every read event observes the same write event in both traces. While the traditional Mazurkiewicz equivalence is control-centric, our new definition is data-centric. We show that our observation equivalence is coarser than the Mazurkiewicz equivalence, and in many cases even exponentially coarser. We devise a DPOR exploration of the trace space, called data-centric DPOR, based on the observation equivalence.","lang":"eng"}],"citation":{"apa":"Chalupa, M., Chatterjee, K., Pavlogiannis, A., Sinha, N., &#38; Vaidya, K. (2018). Data-centric dynamic partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158119\">https://doi.org/10.1145/3158119</a>","mla":"Chalupa, Marek, et al. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 31, Association for Computing Machinery, 2018, doi:<a href=\"https://doi.org/10.1145/3158119\">10.1145/3158119</a>.","ieee":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, and K. Vaidya, “Data-centric dynamic partial order reduction,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2018.","chicago":"Chalupa, Marek, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. “Data-Centric Dynamic Partial Order Reduction.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2018. <a href=\"https://doi.org/10.1145/3158119\">https://doi.org/10.1145/3158119</a>.","ista":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. 2018. Data-centric dynamic partial order reduction. Proceedings of the ACM on Programming Languages. 2(POPL), 31.","ama":"Chalupa M, Chatterjee K, Pavlogiannis A, Sinha N, Vaidya K. Data-centric dynamic partial order reduction. <i>Proceedings of the ACM on Programming Languages</i>. 2018;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158119\">10.1145/3158119</a>","short":"M. Chalupa, K. Chatterjee, A. Pavlogiannis, N. Sinha, K. Vaidya, Proceedings of the ACM on Programming Languages 2 (2018)."},"doi":"10.1145/3158119","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5448"},{"id":"5456","relation":"earlier_version","status":"public"}]},"scopus_import":"1"},{"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","status":"public","tmp":{"short":"CC BY (4.0)","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)"},"date_updated":"2025-04-15T07:26:20Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Choudhary, Bhavya","first_name":"Bhavya","last_name":"Choudhary"},{"orcid":"0000-0002-8943-0722","full_name":"Pavlogiannis, Andreas","first_name":"Andreas","last_name":"Pavlogiannis","id":"49704004-F248-11E8-B48F-1D18A9856A87"}],"title":"Optimal Dyck reachability for data-dependence and Alias analysis","article_type":"original","acknowledgement":"The research was partly supported by Austrian Science Fund (FWF) Grant No P23499-N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), and ERC Start grant (279307: Graph Games).\r\n","day":"27","department":[{"_id":"KrCh"}],"ec_funded":1,"date_published":"2017-12-27T00:00:00Z","publication_identifier":{"eissn":["2475-1421"]},"arxiv":1,"external_id":{"arxiv":["1910.00241"]},"oa":1,"article_number":"30","oa_version":"Published Version","date_created":"2021-12-05T23:01:48Z","project":[{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications"},{"call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"_id":"10416","publication":"Proceedings of the ACM on Programming Languages","file":[{"creator":"cchlebak","file_name":"2017_ACMProgLang_Chatterjee.pdf","relation":"main_file","date_created":"2021-12-07T08:06:28Z","checksum":"faa3f7b3fe8aab84b50ed805c26a0ee5","file_size":460188,"date_updated":"2021-12-07T08:06:28Z","content_type":"application/pdf","success":1,"access_level":"open_access","file_id":"10421"}],"quality_controlled":"1","conference":{"location":"Los Angeles, CA, United States","name":"POPL: Programming Languages","end_date":"2018-01-13","start_date":"2018-01-07"},"ddc":["000"],"year":"2017","language":[{"iso":"eng"}],"volume":2,"article_processing_charge":"No","month":"12","issue":"POPL","file_date_updated":"2021-12-07T08:06:28Z","scopus_import":"1","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"5455"}]},"doi":"10.1145/3158118","citation":{"ista":"Chatterjee K, Choudhary B, Pavlogiannis A. 2017. Optimal Dyck reachability for data-dependence and Alias analysis. Proceedings of the ACM on Programming Languages. 2(POPL), 30.","ieee":"K. Chatterjee, B. Choudhary, and A. Pavlogiannis, “Optimal Dyck reachability for data-dependence and Alias analysis,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","chicago":"Chatterjee, Krishnendu, Bhavya Choudhary, and Andreas Pavlogiannis. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158118\">https://doi.org/10.1145/3158118</a>.","ama":"Chatterjee K, Choudhary B, Pavlogiannis A. Optimal Dyck reachability for data-dependence and Alias analysis. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158118\">10.1145/3158118</a>","short":"K. Chatterjee, B. Choudhary, A. Pavlogiannis, Proceedings of the ACM on Programming Languages 2 (2017).","apa":"Chatterjee, K., Choudhary, B., &#38; Pavlogiannis, A. (2017). Optimal Dyck reachability for data-dependence and Alias analysis. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158118\">https://doi.org/10.1145/3158118</a>","mla":"Chatterjee, Krishnendu, et al. “Optimal Dyck Reachability for Data-Dependence and Alias Analysis.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 30, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158118\">10.1145/3158118</a>."},"abstract":[{"lang":"eng","text":"A fundamental algorithmic problem at the heart of static analysis is Dyck reachability. The input is a graph where the edges are labeled with different types of opening and closing parentheses, and the reachability information is computed via paths whose parentheses are properly matched. We present new results for Dyck reachability problems with applications to alias analysis and data-dependence analysis. Our main contributions, that include improved upper bounds as well as lower bounds that establish optimality guarantees, are as follows: First, we consider Dyck reachability on bidirected graphs, which is the standard way of performing field-sensitive points-to analysis. Given a bidirected graph with n nodes and m edges, we present: (i) an algorithm with worst-case running time O(m + n · α(n)), where α(n) is the inverse Ackermann function, improving the previously known O(n2) time bound; (ii) a matching lower bound that shows that our algorithm is optimal wrt to worst-case complexity; and (iii) an optimal average-case upper bound of O(m) time, improving the previously known O(m · logn) bound. Second, we consider the problem of context-sensitive data-dependence analysis, where the task is to obtain analysis summaries of library code in the presence of callbacks. Our algorithm preprocesses libraries in almost linear time, after which the contribution of the library in the complexity of the client analysis is only linear, and only wrt the number of call sites. Third, we prove that combinatorial algorithms for Dyck reachability on general graphs with truly sub-cubic bounds cannot be obtained without obtaining sub-cubic combinatorial algorithms for Boolean Matrix Multiplication, which is a long-standing open problem. Thus we establish that the existing combinatorial algorithms for Dyck reachability are (conditionally) optimal for general graphs. We also show that the same hardness holds for graphs of constant treewidth. Finally, we provide a prototype implementation of our algorithms for both alias analysis and data-dependence analysis. Our experimental evaluation demonstrates that the new algorithms significantly outperform all existing methods on the two problems, over real-world benchmarks."}],"publication_status":"published","corr_author":"1","type":"journal_article","publisher":"Association for Computing Machinery","has_accepted_license":"1","intvolume":"         2"},{"ddc":["000"],"year":"2017","conference":{"location":"Los Angeles, CA, United States","end_date":"2018-01-13","name":"POPL: Programming Languages","start_date":"2018-01-07"},"quality_controlled":"1","volume":2,"language":[{"iso":"eng"}],"article_processing_charge":"No","issue":"POPL","month":"12","doi":"10.1145/3158121","scopus_import":"1","abstract":[{"text":"We present a new proof rule for proving almost-sure termination of probabilistic programs, including those that contain demonic non-determinism. An important question for a probabilistic program is whether the probability mass of all its diverging runs is zero, that is that it terminates \"almost surely\". Proving that can be hard, and this paper presents a new method for doing so. It applies directly to the program's source code, even if the program contains demonic choice. Like others, we use variant functions (a.k.a. \"super-martingales\") that are real-valued and decrease randomly on each loop iteration; but our key innovation is that the amount as well as the probability of the decrease are parametric. We prove the soundness of the new rule, indicate where its applicability goes beyond existing rules, and explain its connection to classical results on denumerable (non-demonic) Markov chains.","lang":"eng"}],"citation":{"ista":"Mciver A, Morgan C, Kaminski BL, Katoen JP. 2017. A new proof rule for almost-sure termination. Proceedings of the ACM on Programming Languages. 2(POPL), 33.","ieee":"A. Mciver, C. Morgan, B. L. Kaminski, and J. P. Katoen, “A new proof rule for almost-sure termination,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL. Association for Computing Machinery, 2017.","chicago":"Mciver, Annabelle, Carroll Morgan, Benjamin Lucien Kaminski, and Joost P Katoen. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2017. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>.","ama":"Mciver A, Morgan C, Kaminski BL, Katoen JP. A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. 2017;2(POPL). doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>","short":"A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).","mla":"Mciver, Annabelle, et al. “A New Proof Rule for Almost-Sure Termination.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 2, no. POPL, 33, Association for Computing Machinery, 2017, doi:<a href=\"https://doi.org/10.1145/3158121\">10.1145/3158121</a>.","apa":"Mciver, A., Morgan, C., Kaminski, B. L., &#38; Katoen, J. P. (2017). A new proof rule for almost-sure termination. <i>Proceedings of the ACM on Programming Languages</i>. Los Angeles, CA, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3158121\">https://doi.org/10.1145/3158121</a>"},"publisher":"Association for Computing Machinery","type":"journal_article","corr_author":"1","publication_status":"published","intvolume":"         2","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-06-18T08:40:04Z","status":"public","author":[{"full_name":"Mciver, Annabelle","first_name":"Annabelle","last_name":"Mciver"},{"full_name":"Morgan, Carroll","last_name":"Morgan","first_name":"Carroll"},{"full_name":"Kaminski, Benjamin Lucien","first_name":"Benjamin Lucien","last_name":"Kaminski"},{"id":"4524F760-F248-11E8-B48F-1D18A9856A87","full_name":"Katoen, Joost P","orcid":"0000-0002-6143-1926","last_name":"Katoen","first_name":"Joost P"}],"main_file_link":[{"url":"https://dl.acm.org/doi/10.1145/3158121","open_access":"1"}],"title":"A new proof rule for almost-sure termination","day":"07","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"acknowledgement":"McIver and Morgan are grateful to David Basin and the Information Security Group at ETH Zürich for hosting a six-month stay in Switzerland, during part of which this work began. And thanks particularly to Andreas Lochbihler, who shared with us the probabilistic termination problem that led to it. They acknowledge the support of ARC grant DP140101119. Part of this work was carried out during the Workshop on Probabilistic Programming Semantics\r\nat McGill University’s Bellairs Research Institute on Barbados organised by Alexandra Silva and\r\nPrakash Panangaden. Kaminski and Katoen are grateful to Sebastian Junges for spotting a flaw in §5.4.","article_type":"original","arxiv":1,"publication_identifier":{"eissn":["2475-1421"]},"date_published":"2017-12-07T00:00:00Z","oa":1,"external_id":{"arxiv":["1711.03588"]},"_id":"10418","date_created":"2021-12-05T23:01:49Z","oa_version":"Published Version","article_number":"33","publication":"Proceedings of the ACM on Programming Languages"}]