{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:03:59Z","timestamp":1784675039509,"version":"3.55.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100012659","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772336, 61802254"],"award-info":[{"award-number":["61772336, 61802254"]}],"id":[{"id":"10.13039\/501100012659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["Starting Grant 279307: Graph Games"],"award-info":[{"award-number":["Starting Grant 279307: Graph Games"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100004316","name":"International Business Machines Corporation","doi-asserted-by":"publisher","award":["IBM PhD Fellowship"],"award-info":[{"award-number":["IBM PhD Fellowship"]}],"id":[{"id":"10.13039\/100004316","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-003"],"award-info":[{"award-number":["ICT15-003"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Shanghai Key Laboratory of Trustworthy Computing","award":["Open Project"],"award-info":[{"award-number":["Open Project"]}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11407-N23 (RiSE\/SHiNE)"],"award-info":[{"award-number":["S11407-N23 (RiSE\/SHiNE)"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"name":"\u00d6sterreichischen Akademie der Wissenschaften","award":["DOC 24956"],"award-info":[{"award-number":["DOC 24956"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>In this work, we consider the almost-sure termination problem for probabilistic programs that asks whether a given probabilistic program terminates with probability 1. Scalable approaches for program analysis often rely on modularity as their theoretical basis. In non-probabilistic programs, the classical variant rule (V-rule) of Floyd-Hoare logic provides the foundation for modular analysis. Extension of this rule to almost-sure termination of probabilistic programs is quite tricky, and a probabilistic variant was proposed by Fioriti and Hermanns in POPL 2015. While the proposed probabilistic variant cautiously addresses the key issue of integrability, we show that the proposed modular rule is still not sound for almost-sure termination of probabilistic programs.<\/jats:p>\n          <jats:p>Besides establishing unsoundness of the previous rule, our contributions are as follows: First, we present a sound modular rule for almost-sure termination of probabilistic programs. Our approach is based on a novel notion of descent supermartingales. Second, for algorithmic approaches, we consider descent supermartingales that are linear and show that they can be synthesized in polynomial time. Finally, we present experimental results on a variety of benchmarks and several natural examples that model various types of nested while loops in probabilistic programs and demonstrate that our approach is able to efficiently prove their almost-sure termination property.<\/jats:p>","DOI":"10.1145\/3360555","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":32,"title":["Modular verification for almost-sure termination of probabilistic programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Mingzhang","family":"Huang","sequence":"first","affiliation":[{"name":"Shanghai Jiao Tong University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"Shanghai Jiao Tong University, China \/ East China Normal University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amir Kafshdar","family":"Goharshady","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_1_2_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_3_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.","author":"Batz Kevin","year":"2019","unstructured":"Kevin Batz , Benjamin Lucien Kaminski , Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019 . Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. In POPL. Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll. 2019. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. In POPL."},{"key":"e_1_2_1_4_1","unstructured":"Michel Berkelaar Kjell Eikland Peter Notebaert etal 2004. lpsolve: Open source (mixed-integer) linear programming system. Eindhoven U. of Technology (2004).  Michel Berkelaar Kjell Eikland Peter Notebaert et al. 2004. lpsolve: Open source (mixed-integer) linear programming system. Eindhoven U. of Technology (2004)."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Olivier Bournez and Florent Garnier. 2005. Proving Positive Almost-Sure Termination. In RTA. 323\u2013337.  Olivier Bournez and Florent Garnier. 2005. Proving Positive Almost-Sure Termination. In RTA. 323\u2013337.","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV. 511\u2013526.  Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV. 511\u2013526.","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_7_1","unstructured":"Krishnendu Chatterjee and Hongfei Fu. 2019. Termination of Nondeterministic Recursive Probabilistic Programs. In VMCAI.  Krishnendu Chatterjee and Hongfei Fu. 2019. Termination of Nondeterministic Recursive Probabilistic Programs. In VMCAI."},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu and Amir Kafshdar Goharshady. 2016a. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In CAV. 3\u201322.  Krishnendu Chatterjee Hongfei Fu and Amir Kafshdar Goharshady. 2016a. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In CAV. 3\u201322.","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_9_1","volume-title":"Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI","author":"Chatterjee Krishnendu","year":"2018","unstructured":"Krishnendu Chatterjee , Hongfei Fu , Amir Kafshdar Goharshady , and Nastaran Okati . 2018 . Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI 2018. 4700\u20134707. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Nastaran Okati. 2018. Computational Approaches for Stochastic Shortest Path on Succinct MDPs. In IJCAI 2018. 4700\u20134707."},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016b. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In POPL. 327\u2013342.  Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016b. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In POPL. 327\u2013342.","DOI":"10.1145\/2914770.2837639"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and \u00d0or\u0111e \u017dikeli\u0107. 2017. Stochastic invariants for probabilistic termination. In POPL. 145\u2013160.  Krishnendu Chatterjee Petr Novotn\u00fd and \u00d0or\u0111e \u017dikeli\u0107. 2017. Stochastic invariants for probabilistic termination. In POPL. 145\u2013160.","DOI":"10.1145\/3093333.3009873"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491423"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Michael Col\u00f3n Sriram Sankaranarayanan and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV. 420\u2013432.  Michael Col\u00f3n Sriram Sankaranarayanan and Henny Sipma. 2003. Linear Invariant Generation Using Non-linear Constraint Solving. In CAV. 420\u2013432.","DOI":"10.1007\/978-3-540-45069-6_39"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Javier Esparza Andreas Gaiser and Stefan Kiefer. 2012. Proving Termination of Probabilistic Programs Using Patterns. In CAV. 123\u2013138.  Javier Esparza Andreas Gaiser and Stefan Kiefer. 2012. Proving Termination of Probabilistic Programs Using Patterns. In CAV. 123\u2013138.","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462153.1462154"},{"key":"e_1_2_1_16_1","volume-title":"A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12","author":"Farkas Julius","year":"1894","unstructured":"Julius Farkas . 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12 ( 1894 ), 457\u2013472. Julius Farkas. 1894. A Fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 12 (1894), 457\u2013472."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_2_1_19_1","volume-title":"Probabilistic NetKAT","author":"Foster Nate","unstructured":"Nate Foster , Dexter Kozen , Konstantinos Mamouras , Mark Reitblatt , and Alexandra Silva . 2016. Probabilistic NetKAT . In ESOP. Springer , 282\u2013309. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. 2016. Probabilistic NetKAT. In ESOP. Springer, 282\u2013309."},{"key":"e_1_2_1_20_1","volume-title":"Church: a language for generative models","author":"Goodman Noah D","unstructured":"Noah D Goodman , Vikash K Mansinghka , Daniel Roy , Keith Bonawitz , and Joshua B Tenenbaum . 2008. Church: a language for generative models . In UAI. AUAI Press , 220\u2013229. Noah D Goodman, Vikash K Mansinghka, Daniel Roy, Keith Bonawitz, and Joshua B Tenenbaum. 2008. Church: a language for generative models. In UAI. AUAI Press, 220\u2013229."},{"key":"e_1_2_1_21_1","unstructured":"Noah D Goodman and Andreas Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org . (2014).  Noah D Goodman and Andreas Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org . (2014)."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429119"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211249"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Mingzhang Huang Hongfei Fu and Krishnendu Chatterjee. 2018. New Approaches for Almost-Sure Termination of Probabilistic Programs. In APLAS. 181\u2013201.  Mingzhang Huang Hongfei Fu and Krishnendu Chatterjee. 2018. New Approaches for Almost-Sure Termination of Probabilistic Programs. In APLAS. 181\u2013201.","DOI":"10.1007\/978-3-030-02768-1_11"},{"key":"e_1_2_1_27_1","volume-title":"Modular Verification for Almost-Sure Termination of Probabilistic Programs. arXiv preprint arXiv:1901.06087","author":"Huang Mingzhang","year":"2019","unstructured":"Mingzhang Huang , Hongfei Fu , Krishnendu Chatterjee , and Amir Kafshdar Goharshady . 2019. Modular Verification for Almost-Sure Termination of Probabilistic Programs. arXiv preprint arXiv:1901.06087 ( 2019 ). Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady. 2019. Modular Verification for Almost-Sure Termination of Probabilistic Programs. arXiv preprint arXiv:1901.06087 (2019)."},{"key":"e_1_2_1_28_1","unstructured":"Claire Jones. 1989. Probabilistic Non-Determinism. Ph.D. Dissertation. The University of Edinburgh.  Claire Jones. 1989. Probabilistic Non-Determinism. Ph.D. Dissertation. The University of Edinburgh."},{"key":"e_1_2_1_29_1","first-page":"1","article-title":"Undecidable Problems for Probabilistic Network Programming","volume":"68","author":"Kahn David M.","year":"2017","unstructured":"David M. Kahn . 2017 . Undecidable Problems for Probabilistic Network Programming . In MFCS. 68 : 1 \u2013 68 :17. David M. Kahn. 2017. Undecidable Problems for Probabilistic Network Programming. In MFCS. 68:1\u201368:17.","journal-title":"MFCS."},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In ESOP. 364\u2013389.  Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In ESOP. 364\u2013389.","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_31_1","volume-title":"On the hardness of analyzing probabilistic programs. Acta Informatica","author":"Kaminski Benjamin Lucien","year":"2018","unstructured":"Benjamin Lucien Kaminski , Joost-Pieter Katoen , and Christoph Matheja . 2018. On the hardness of analyzing probabilistic programs. Acta Informatica ( 2018 ), 1\u201331. Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2018. On the hardness of analyzing probabilistic programs. Acta Informatica (2018), 1\u201331."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264565"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_14"},{"key":"e_1_2_1_34_1","unstructured":"Martin Lukasiewycz. 2008. JavaILP - Java Interface to ILP Solvers http:\/\/javailp.sourceforge.net\/. (2008). http:\/\/javailp. sourceforge.net\/  Martin Lukasiewycz. 2008. JavaILP - Java Interface to ILP Solvers http:\/\/javailp.sourceforge.net\/. (2008). http:\/\/javailp. sourceforge.net\/"},{"key":"e_1_2_1_35_1","volume-title":"P\u00f3lya urn models","author":"Mahmoud Hosam","unstructured":"Hosam Mahmoud . 2008. P\u00f3lya urn models . Chapman and Hall\/CRC. Hosam Mahmoud. 2008. P\u00f3lya urn models. Chapman and Hall\/CRC."},{"key":"e_1_2_1_36_1","volume-title":"Foundations of statistical natural language processing","author":"Manning Christopher D","unstructured":"Christopher D Manning , Christopher D Manning , and Hinrich Sch\u00fctze . 1999. Foundations of statistical natural language processing . MIT press . Christopher D Manning, Christopher D Manning, and Hinrich Sch\u00fctze. 1999. Foundations of statistical natural language processing. MIT press."},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Colin McDiarmid. 1998. Concentration. In Probabilistic Methods for Algorithmic Discrete Mathematics. 195\u2013248.  Colin McDiarmid. 1998. Concentration. In Probabilistic Methods for Algorithmic Discrete Mathematics. 195\u2013248.","DOI":"10.1007\/978-3-662-12788-9_6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"Annabelle McIver and Carroll Morgan. 2004. Developing and Reasoning About Probabilistic Programs in pGCL. In PSSE. 123\u2013155.  Annabelle McIver and Carroll Morgan. 2004. Developing and Reasoning About Probabilistic Programs in pGCL. In PSSE. 123\u2013155.","DOI":"10.1007\/11889229_4"},{"key":"e_1_2_1_39_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan . 2005. Abstraction , Refinement and Proof for Probabilistic Systems . Springer . Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"Van Chan Ngo Quentin Carbonneaux and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In PLDI. 496\u2013512.  Van Chan Ngo Quentin Carbonneaux and Jan Hoffmann. 2018. Bounded expectations: resource analysis for probabilistic programs. In PLDI. 496\u2013512.","DOI":"10.1145\/3296979.3192394"},{"key":"e_1_2_1_42_1","volume-title":"Joost-Pieter Katoen, and Christoph Matheja.","author":"Olmedo Federico","year":"2016","unstructured":"Federico Olmedo , Benjamin Lucien Kaminski , Joost-Pieter Katoen, and Christoph Matheja. 2016 . Reasoning about Recursive Probabilistic Programs. In LICS. 672\u2013681. Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In LICS. 672\u2013681."},{"key":"e_1_2_1_43_1","volume-title":"Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning","volume":"22","author":"Roy DM","year":"2008","unstructured":"DM Roy , VK Mansinghka , ND Goodman , and JB Tenenbaum . 2008 . A stochastic programming perspective on nonparametric Bayes . In Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning , Vol. 22 . 26. DM Roy, VK Mansinghka, ND Goodman, and JB Tenenbaum. 2008. A stochastic programming perspective on nonparametric Bayes. In Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning, Vol. 22. 26."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27864-1_7"},{"key":"e_1_2_1_45_1","volume-title":"Combinatorial Optimization - Polyhedra and Efficiency","author":"Schrijver Alexander","unstructured":"Alexander Schrijver . 2003. Combinatorial Optimization - Polyhedra and Efficiency . Springer . Alexander Schrijver. 2003. Combinatorial Optimization - Polyhedra and Efficiency. Springer."},{"key":"e_1_2_1_46_1","volume-title":"ACM SIGPLAN Notices","volume":"50","author":"\u015acibior Adam","year":"2015","unstructured":"Adam \u015acibior , Zoubin Ghahramani , and Andrew D Gordon . 2015 . Practical probabilistic programming with monads . In ACM SIGPLAN Notices , Vol. 50 . ACM, 165\u2013176. Adam \u015acibior, Zoubin Ghahramani, and Andrew D Gordon. 2015. Practical probabilistic programming with monads. In ACM SIGPLAN Notices, Vol. 50. ACM, 165\u2013176."},{"key":"e_1_2_1_47_1","doi-asserted-by":"crossref","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor meets Scott: semantic foundations for probabilistic networks. In POPL. 557\u2013571.  Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor meets Scott: semantic foundations for probabilistic networks. In POPL. 557\u2013571.","DOI":"10.1145\/3093333.3009843"},{"key":"e_1_2_1_48_1","first-page":"93","article-title":"Probabilistic algorithms in robotics","volume":"21","author":"Thrun Sebastian","year":"2000","unstructured":"Sebastian Thrun . 2000 . Probabilistic algorithms in robotics . Ai Magazine 21 , 4 (2000), 93 . Sebastian Thrun. 2000. Probabilistic algorithms in robotics. Ai Magazine 21, 4 (2000), 93.","journal-title":"Ai Magazine"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/504729.504754"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064899.3064910"},{"key":"e_1_2_1_51_1","volume-title":"Reps","author":"Wang Di","year":"2018","unstructured":"Di Wang , Jan Hoffmann , and Thomas W . Reps . 2018 . PMAF: an algebraic framework for static analysis of probabilistic programs. In PLDI. 513\u2013528. Di Wang, Jan Hoffmann, and Thomas W. Reps. 2018. PMAF: an algebraic framework for static analysis of probabilistic programs. In PLDI. 513\u2013528."},{"key":"e_1_2_1_52_1","volume-title":"Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi.","author":"Wang Peixin","year":"2019","unstructured":"Peixin Wang , Hongfei Fu , Amir Kafshdar Goharshady , Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019 . Cost Analysis of Nondeterministic Probabilistic Programs. In PLDI. 204\u2013220. Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi. 2019. Cost Analysis of Nondeterministic Probabilistic Programs. In PLDI. 204\u2013220."},{"key":"e_1_2_1_53_1","volume-title":"Probability with Martingales","author":"Williams David","unstructured":"David Williams . 1991. Probability with Martingales . Cambridge University Press . David Williams. 1991. Probability with Martingales. Cambridge University Press."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360555","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360555","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:58Z","timestamp":1750202578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360555"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":53,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360555"],"URL":"https:\/\/doi.org\/10.1145\/3360555","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}