{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:57:13Z","timestamp":1770285433474,"version":"3.49.0"},"reference-count":86,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["863818"],"award-info":[{"award-number":["863818"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["GA23-06963S"],"award-info":[{"award-number":["GA23-06963S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>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.<\/jats:p>\n          <jats:p>\n            CCS Concepts: \u2022\n            <jats:bold>Theory of computation \u2192 Program verification; Program analysis; \u2022 Software and its engineering \u2192 Formal software verification; \u2022 Mathematics of computing \u2192 Probability and statistics<\/jats:bold>\n            .\n          <\/jats:p>","DOI":"10.1145\/3656462","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"2098-2122","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Equivalence and Similarity Refutation for Probabilistic Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4561-241X","authenticated-orcid":false,"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8595-0587","authenticated-orcid":false,"given":"Ehsan Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"IST Austria, Klosterneuburg, Austria"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5026-4392","authenticated-orcid":false,"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"Masaryk University, Brno, Czechia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4681-1699","authenticated-orcid":false,"given":"\u0110or\u0111e","family":"\u017dikeli\u0107","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434333"},{"key":"e_1_3_1_4_1","unstructured":"Alejandro Aguirre Gilles Barthe Justin Hsu and Alexandra Silva. 2018. Almost Sure Productivity. In ICALP."},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158146"},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","unstructured":"Ali Asadi Krishnendu Chatterjee Hongfei Fu Amir Kafshdar Goharshady and Mohammad Mahdavi. 2021. Polynomial reachability witnesses via Stellensatze. In PLDI.","DOI":"10.1145\/3453483.3454076"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_3_1_8_1","doi-asserted-by":"crossref","unstructured":"Jialu Bao Nitesh Trivedi Drashti Pathak Justin Hsu and Subhajit Roy. 2022. Data-Driven Invariant Learning for Probabilistic Programs. In CAV.","DOI":"10.21203\/rs.3.rs-3162619\/v1"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Marco Gaboardi Benjamin Gregoire Justin Hsu and Pierre-Yves Strub. 2016. Proving Differential Privacy via Probabilistic Couplings. In LICS.","DOI":"10.1145\/2933575.2934554"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2893582.2893591"},{"key":"e_1_3_1_12_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Benjamin Gregoire and Santiago Zanella Beguelin. 2009. Formal certification of code-based cryptographic proofs. In POPL.","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3487063"},{"key":"e_1_3_1_14_1","article-title":"Foundations of probabilistic programming","author":"Barthe Gilles","year":"2020","unstructured":"Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. 2020. Foundations of probabilistic programming. Cambridge University Press.","journal-title":"Cambridge University Press"},{"key":"e_1_3_1_15_1","article-title":"Testing Closeness of Discrete Distributions","author":"Batu Tugkan","year":"2013","unstructured":"Tugkan Batu, Lance Fortnow, Ronitt Rubinfeld, Warren D. Smith, and Patrick White. 2013. Testing Closeness of Discrete Distributions. J. ACM 60, 1 (2013).","journal-title":"J. ACM 60, 1 (2013)"},{"key":"e_1_3_1_16_1","doi-asserted-by":"crossref","unstructured":"Kevin Batz Mingshuai Chen Sebastian Junges Benjamin Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2023. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. In TACAS.","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Raven Beutner C.-H. Luke Ong and Fabian Zaiser. 2022. Guaranteed bounds for posterior inference in universal probabilistic programming. In PLDI.","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_3_1_18_1","article-title":"Pyro: Deep Universal Probabilistic Programming","author":"Bingham Eli","year":"2019","unstructured":"Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. 2019. Pyro: Deep Universal Probabilistic Programming. J.Mach. Learn. Res. 20 (2019).","journal-title":"J.Mach. Learn. Res. 20 (2019)"},{"key":"e_1_3_1_19_1","article-title":"A survey on distribution testing: Your data is big","author":"Canonne Clement L","year":"2020","unstructured":"Clement L Canonne. 2020. A survey on distribution testing: Your data is big. But is it blue? Theory of Computing (2020).","journal-title":"But is it blue? Theory of Computing (2020)"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV.","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_1_21_1","doi-asserted-by":"crossref","unstructured":"Sourav Chakraborty and Kuldeep S. Meel. 2019. On Testing of Uniform Samplers. In AAAI.","DOI":"10.1609\/aaai.v33i01.33017777"},{"key":"e_1_3_1_22_1","doi-asserted-by":"crossref","unstructured":"Siu-on Chan Ilias Diakonikolas Paul Valiant and Gregory Valiant. 2014. Optimal Algorithms for Testing Closeness of Discrete Distributions. In SODA.","DOI":"10.1137\/1.9781611973402.88"},{"key":"e_1_3_1_23_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz \u2018s. In CAV.","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu Amir Kafshdar Goharshady and Ehsan Kafshdar Goharshady. 2020. Polynomial invariant generation for non-deterministic recursive programs. In PLDI.","DOI":"10.1145\/3385412.3385969"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3174800"},{"key":"e_1_3_1_26_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Amir Kafshdar Goharshady Tobias Meggendorfer and Dorde Zikelic. 2022. Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. In CAV.","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Ehsan Kafshdar Goharshady Petr Novotny Jiri Zarevucky and Dorde Zikelic. 2021. On Lexicographic Proof Rules for Probabilistic Termination. In FM.","DOI":"10.1007\/978-3-030-90870-6_33"},{"key":"e_1_3_1_28_1","article-title":"Equivalence and Similarity Refutation for Probabilistic Programs","author":"Chatterjee Krishnendu","year":"2024","unstructured":"Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotny, and Dorde Zikelic. 2024. Equivalence and Similarity Refutation for Probabilistic Programs. arXiv:2404.03430 [cs.PL]","journal-title":"arXiv:2404.03430 [cs.PL]"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Petr Novotny and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In POPL.","DOI":"10.1145\/3093333.3009873"},{"key":"e_1_3_1_30_1","doi-asserted-by":"crossref","unstructured":"Swarat Chaudhuri Sumit Gulwani and Roberto Lublinerman. 2010. Continuity analysis of programs. In POPL.","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_1_31_1","unstructured":"Mingshuai Chen Joost-Pieter Katoen Lutz Klinkenberg and Tobias Winkler. 2022. Does a Program Yield the Right Distribution? - Verifying Probabilistic Programs via Generating Functions. In CAV."},{"key":"e_1_3_1_32_1","doi-asserted-by":"crossref","unstructured":"Taolue Chen and Stefan Kiefer. 2014. On the Total Variation Distance of Labelled Markov Chains. In CSL-LICS.","DOI":"10.1145\/2603088.2603099"},{"key":"e_1_3_1_33_1","unstructured":"Ezgi Qigek Gilles Barthe Marco Gaboardi Deepak Garg and Jan Hoffmann. 2017. Relational cost analysis. In POPL."},{"key":"e_1_3_1_34_1","doi-asserted-by":"crossref","unstructured":"Ryan Culpepper and Andrew Cobb. 2017. Contextual equivalence for probabilistic programs with continuous random variables and scoring. In ESOP.","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_3_1_35_1","unstructured":"Marco F. Cusumano-Towner and Vikash K. Mansinghka. 2017. AIDE: An algorithm for measuring the accuracy of probabilistic inference algorithms. In NIPS."},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.10.006"},{"key":"e_1_3_1_37_1","article-title":"An Easy to Interpret Diagnostic for Approximate Inference: Symmetric Divergence Over Simulations","author":"Domke Justin","year":"2021","unstructured":"Justin Domke. 2021. An Easy to Interpret Diagnostic for Approximate Inference: Symmetric Divergence Over Simulations. CoRR abs\/2103.01030 (2021).","journal-title":"CoRR abs\/2103.01030 (2021)"},{"key":"e_1_3_1_38_1","doi-asserted-by":"crossref","unstructured":"Saikat Dutta Owolabi Legunsen Zixin Huang and Sasa Misailovic. 2018. Testing probabilistic programming systems. In FSE.","DOI":"10.1145\/3236024.3236057"},{"key":"e_1_3_1_39_1","doi-asserted-by":"crossref","unstructured":"Saikat Dutta Wenxian Zhang Zixin Huang and Sasa Misailovic. 2019. Storm: program reduction for testing and debugging probabilistic programming systems. In FSE.","DOI":"10.1145\/3338906.3338972"},{"key":"e_1_3_1_40_1","doi-asserted-by":"crossref","unstructured":"Paul Feautrier and Laure Gonnord. 2010. Accelerated Invariant Generation for C Programs with Aspic and C2fsm. In TAPAS@SAS.","DOI":"10.1016\/j.entcs.2010.09.014"},{"key":"e_1_3_1_41_1","doi-asserted-by":"crossref","unstructured":"Dennis Felsing Sarah Grebing Vladimir Klebanov Philipp Rummer and Mattias Ulbrich. 2014. Automating regression verification. In ASE.","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_3_1_42_1","doi-asserted-by":"crossref","unstructured":"Nate Foster Dexter Kozen Konstantinos Mamouras Mark Reitblatt and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP.","DOI":"10.1007\/978-3-662-49498-1_12"},{"key":"e_1_3_1_43_1","doi-asserted-by":"crossref","unstructured":"Timon Gehr Sasa Misailovic and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In CAV.","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.3102\/1076998615606113"},{"key":"e_1_3_1_45_1","doi-asserted-by":"crossref","unstructured":"Zoubin Ghahramani. 2015. Probabilistic machine learning and artificial intelligence. Nat. 521 7553 (2015) 452-459.","DOI":"10.1038\/nature14541"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1472"},{"key":"e_1_3_1_47_1","unstructured":"Noah D. Goodman Vikash K. Mansinghka Daniel M. Roy Kallista A. Bonawitz and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In UAI."},{"key":"e_1_3_1_48_1","doi-asserted-by":"crossref","unstructured":"Andrew D. Gordon Thomas A. Henzinger Aditya V. Nori and Sriram K. Rajamani. 2014. Probabilistic programming. In FOSE.","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_1_49_1","unstructured":"Roger B. Grosse Siddharth Ancha and Daniel M. Roy. 2016. Measuring the reliability of MCMC inference with bidirectional Monte Carlo. In NIPS."},{"key":"e_1_3_1_50_1","article-title":"Sandwiching the marginal likelihood using bidirectional Monte Carlo","author":"Grosse Roger B.","year":"2015","unstructured":"Roger B. Grosse, Zoubin Ghahramani, and Ryan P. Adams. 2015. Sandwiching the marginal likelihood using bidirectional Monte Carlo. CoRR abs\/1511.02543 (2015).","journal-title":"CoRR abs\/1511.02543 (2015)"},{"key":"e_1_3_1_51_1","unstructured":"Gurobi Optimization LLC. 2023. Gurobi Optimizer Reference Manual. https:\/\/www.gurobi.com"},{"key":"e_1_3_1_52_1","article-title":"Representing polynomials by positive linear functions on compact convex polyhedra","author":"Handelman David","year":"1988","unstructured":"David Handelman. 1988. Representing polynomials by positive linear functions on compact convex polyhedra. Pacific J. Math. 132, 1 (1988).","journal-title":"Pacific J. Math. 132, 1 (1988)"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_1_54_1","doi-asserted-by":"crossref","unstructured":"Leen Helmink M. P. A. Sellink and Frits W. Vaandrager. 1993. Proof-Checking a Data Link Protocol. In TYPES.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"e_1_3_1_55_1","doi-asserted-by":"crossref","unstructured":"Zixin Huang Zhenbang Wang and Sasa Misailovic. 2018. PSense: Automatic Sensitivity Analysis for Probabilistic Programs. In ATVA.","DOI":"10.1007\/978-3-030-01090-4_23"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_3_1_57_1","doi-asserted-by":"crossref","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes ofRandomized Algorithms. J. ACM 65 5 (2018).","DOI":"10.1145\/3208102"},{"key":"e_1_3_1_58_1","unstructured":"Stefan Kiefer. 2018. On Computing the Total Variation Distance of Hidden Markov Models. In ICALP."},{"key":"e_1_3_1_59_1","doi-asserted-by":"crossref","unstructured":"Stefan Kiefer Andrzej S. Murawski Joel Ouaknine Bjorn Wachter and James Worrell. 2011. Language Equivalence for Probabilistic Automata. In CAV.","DOI":"10.1007\/978-3-642-22110-1_42"},{"key":"e_1_3_1_60_1","unstructured":"Stefan Kiefer and Qiyi Tang. 2020. Comparing Labelled Markov Decision Processes. In FSTTCS."},{"key":"e_1_3_1_61_1","doi-asserted-by":"crossref","unstructured":"Satoshi Kura Natsuki Urabe and Ichiro Hasuo. 2019. Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments. In TACAS.","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_3_1_63_1","unstructured":"Axel Legay Andrzej S. Murawski Joel Ouaknine and James Worrell. 2008. On Automated Verification of Probabilistic Programs. In TACAS."},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_3_1_65_1","article-title":"Markov chains and stochastic stability","author":"Meyn Sean P","year":"2012","unstructured":"Sean P Meyn and Richard L Tweedie. 2012. Markov chains and stochastic stability. Springer Science & Business Media.","journal-title":"Springer Science & Business Media"},{"key":"e_1_3_1_66_1","doi-asserted-by":"crossref","unstructured":"Andrzej S. Murawski and Joel Ouaknine. 2005. On Probabilistic Program Equivalence and Refinement. In CONCUR.","DOI":"10.1007\/11539452_15"},{"key":"e_1_3_1_67_1","unstructured":"Chandrakana Nandi Dan Grossman Adrian Sampson Todd Mytkowicz and Kathryn S. McKinley. 2017. Debugging probabilistic programs. In MAPL@PLDI."},{"key":"e_1_3_1_68_1","unstructured":"Van Chan Ngo Quentin Carbonneaux and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In PLDI."},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_3_1_70_1","article-title":"Fixpoint induction and proofs of program properties","author":"Park David","year":"1969","unstructured":"David Park. 1969. Fixpoint induction and proofs of program properties. Machine intelligence 5 (1969).","journal-title":"Machine intelligence 5 (1969)"},{"key":"e_1_3_1_71_1","doi-asserted-by":"crossref","unstructured":"Nimrod Partush and Eran Yahav. 2013. Abstract Semantic Differencing for Numerical Programs. In SAS.","DOI":"10.1007\/978-3-642-38856-9_14"},{"key":"e_1_3_1_72_1","doi-asserted-by":"crossref","unstructured":"Nimrod Partush and Eran Yahav. 2014. Abstract semantic differencing via speculative correlation. In OOPSLA.","DOI":"10.1145\/2660193.2660245"},{"key":"e_1_3_1_73_1","unstructured":"Weihao Qu Marco Gaboardi and Deepak Garg. 2021. Relational cost analysis in a functional-imperative setting. (2021)."},{"key":"e_1_3_1_74_1","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan Aleksandar Chakarov and Sumit Gulwani. 2013. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In PLDI.","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_1_75_1","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan Henny B. Sipma and Zohar Manna. 2004. Constraint-Based Linear-Relations Analysis. In SAS.","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_3_1_77_1","article-title":"Probabilistic Algorithms in Robotics","author":"Thrun Sebastian","year":"2000","unstructured":"Sebastian Thrun. 2000. Probabilistic Algorithms in Robotics. AIMag. 21, 4 (2000).","journal-title":"AIMag. 21, 4 (2000)"},{"key":"e_1_3_1_78_1","doi-asserted-by":"crossref","unstructured":"Mathieu Tracol Josee Desharnais and Abir Zhioua. 2011. Computing Distances between Probabilistic Automata. In QAPL.","DOI":"10.4204\/EPTCS.57.11"},{"key":"e_1_3_1_79_1","unstructured":"Dustin Tran Matthew D. Hoffman Rif A. Saurous Eugene Brevdo Kevin Murphy and David M. Blei. 2017. Deep probabilistic programming. In ICLR."},{"key":"e_1_3_1_80_1","article-title":"An Introduction to Probabilistic Programming","author":"Meent Jan-Willem van de","year":"2018","unstructured":"Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR abs\/1809.10756 (2018). http:\/\/arxiv.org\/abs\/1809.10756","journal-title":"CoRR abs\/1809.10756 (2018)"},{"key":"e_1_3_1_81_1","article-title":"Topics in optimal transportation","author":"Villani Cedric","year":"2021","unstructured":"Cedric Villani. 2021. Topics in optimal transportation. Vol. 58. American Mathematical Soc.","journal-title":"Vol. 58. American Mathematical Soc"},{"key":"e_1_3_1_82_1","doi-asserted-by":"crossref","unstructured":"Di Wang Jan Hoffmann and Thomas W. Reps. 2021. Central moment analysis for cost accumulators in probabilistic programs. In PLDI.","DOI":"10.1145\/3410293"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371093"},{"key":"e_1_3_1_84_1","doi-asserted-by":"crossref","unstructured":"Peixin Wang Hongfei Fu Amir Kafshdar Goharshady Krishnendu Chatterjee Xudong Qin and Wenjun Shi. 2019. Cost analysis of nondeterministic probabilistic programs. In PLDI.","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_3_1_85_1","article-title":"Probability with Martingales","author":"Williams David","year":"1991","unstructured":"David Williams. 1991. Probability with Martingales. Cambridge University Press.","journal-title":"Cambridge University Press"},{"key":"e_1_3_1_86_1","unstructured":"Wolfram Research Inc. 2022. Mathematica 13.2. https:\/\/www.wolfram.com"},{"key":"e_1_3_1_87_1","doi-asserted-by":"crossref","unstructured":"Dorde Zikelic Bor-Yuh Evan Chang Pauline Bolignano and Franco Raimondi. 2022. Differential cost analysis with simultaneous potentials and anti-potentials. In PLDI.","DOI":"10.1145\/3519939.3523435"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656462","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656462","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:51Z","timestamp":1751661831000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656462"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":86,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656462"],"URL":"https:\/\/doi.org\/10.1145\/3656462","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}