{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:16:02Z","timestamp":1770272162752,"version":"3.49.0"},"reference-count":102,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100012166","name":"National Key Research and Development Program of China","doi-asserted-by":"publisher","award":["2022YFA1005101"],"award-info":[{"award-number":["2022YFA1005101"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62192732, 62032024"],"award-info":[{"award-number":["62192732, 62032024"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["787914"],"award-info":[{"award-number":["787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100018694","name":"HORIZON EUROPE Marie Sklodowska-Curie Actions","doi-asserted-by":"publisher","award":["101008233"],"award-info":[{"award-number":["101008233"]}],"id":[{"id":"10.13039\/100018694","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to almost-surely terminating programs -- as is the case for existing rules -- and can be used to establish non-trivial lower bounds on, e.g., termination probabilities and expected values, for possibly divergent probabilistic loops, e.g., the well-known three-dimensional random walk on a lattice.<\/jats:p>","DOI":"10.1145\/3586051","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"696-726","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Lower Bounds for Possibly Divergent Probabilistic Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5352-4954","authenticated-orcid":false,"given":"Shenghua","family":"Feng","sequence":"first","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[{"name":"Zhejiang University, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4260-8340","authenticated-orcid":false,"given":"Han","family":"Su","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"Saarland University, Germany \/ University College London, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"SFM (LNCS","volume":"121","author":"\u00c1brah\u00e1m Erika","year":"2014","unstructured":"Erika \u00c1brah\u00e1m , Bernd Becker , Christian Dehnert , Nils Jansen , Joost-Pieter Katoen , and Ralf Wimmer . 2014 . Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey . In SFM (LNCS , Vol. 8483). Springer, 65\u2013 121 . Erika \u00c1brah\u00e1m, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, and Ralf Wimmer. 2014. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey. In SFM (LNCS, Vol. 8483). Springer, 65\u2013121."},{"key":"e_1_2_1_2_1","volume-title":"Proc. ACM Program. Lang., 5, POPL","author":"Aguirre Alejandro","year":"2021","unstructured":"Alejandro Aguirre , Gilles Barthe , Justin Hsu , Benjamin Lucien Kaminski , Joost-Pieter Katoen , and Christoph Matheja . 2021 . A Pre-Expectation Calculus for Probabilistic Sensitivity . Proc. ACM Program. Lang., 5, POPL (2021), 1\u201328. Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2021. A Pre-Expectation Calculus for Probabilistic Sensitivity. Proc. ACM Program. Lang., 5, POPL (2021), 1\u201328."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_1_5_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_6_1","volume-title":"CAV (II) (LNCS","volume":"180","author":"Baier Christel","year":"2017","unstructured":"Christel Baier , Joachim Klein , Linda Leuschner , David Parker , and Sascha Wunderlich . 2017 . Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes . In CAV (II) (LNCS , Vol. 10426). Springer, 160\u2013 180 . Christel Baier, Joachim Klein, Linda Leuschner, David Parker, and Sascha Wunderlich. 2017. Ensuring the Reliability of Your Model Checker: Interval Iteration for Markov Decision Processes. In CAV (II) (LNCS, Vol. 10426). Springer, 160\u2013180."},{"key":"e_1_2_1_7_1","volume-title":"FoSSaCS (LNCS","volume":"81","author":"Baldan Paolo","year":"2021","unstructured":"Paolo Baldan , Richard Eggert , Barbara K\u00f6nig , and Tommaso Padoan . 2021 . Fixpoint Theory \u2013 Upside Down . In FoSSaCS (LNCS , Vol. 12650). Springer, 62\u2013 81 . Paolo Baldan, Richard Eggert, Barbara K\u00f6nig, and Tommaso Padoan. 2021. Fixpoint Theory \u2013 Upside Down. In FoSSaCS (LNCS, Vol. 12650). Springer, 62\u201381."},{"key":"e_1_2_1_8_1","volume-title":"CAV (I) (LNCS","author":"Bao Jialu","unstructured":"Jialu Bao , Nitesh Trivedi , Drashti Pathak , Justin Hsu , and Subhajit Roy . 2022. Data-Driven Invariant Learning for Probabilistic Programs . In CAV (I) (LNCS , Vol. 13371). Springer, 33\u2013 54 . Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu, and Subhajit Roy. 2022. Data-Driven Invariant Learning for Probabilistic Programs. In CAV (I) (LNCS, Vol. 13371). Springer, 33\u201354."},{"key":"e_1_2_1_9_1","volume-title":"Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe , Thomas Espitau , Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu . 2016 . Synthesizing Probabilistic Invariants via Doob\u2019s Decomposition. In CAV (I) (LNCS , Vol. 9779). Springer, 43\u2013 61 . Gilles Barthe, Thomas Espitau, Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu. 2016. Synthesizing Probabilistic Invariants via Doob\u2019s Decomposition. In CAV (I) (LNCS, Vol. 9779). Springer, 43\u201361."},{"key":"e_1_2_1_10_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"Barthe Gilles","year":"2018","unstructured":"Gilles Barthe , Thomas Espitau , Benjamin Gr\u00e9goire , Justin Hsu , and Pierre-Yves Strub . 2018 . Proving Expected Sensitivity of Probabilistic Programs . Proc. ACM Program. Lang., 2, POPL (2018), 57:1\u201357:29. Gilles Barthe, Thomas Espitau, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2018. Proving Expected Sensitivity of Probabilistic Programs. Proc. ACM Program. Lang., 2, POPL (2018), 57:1\u201357:29."},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire and Santiago Zanella B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In POPL. ACM 90\u2013101. \t\t\t\t  Gilles Barthe Benjamin Gr\u00e9goire and Santiago Zanella B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In POPL. ACM 90\u2013101.","DOI":"10.1145\/1594834.1480894"},{"key":"e_1_2_1_12_1","volume-title":"MPC (LNCS","volume":"6","author":"Barthe Gilles","year":"2012","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Santiago Zanella B\u00e9guelin . 2012 . Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs . In MPC (LNCS , Vol. 7342). Springer, 1\u2013 6 . Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella B\u00e9guelin. 2012. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In MPC (LNCS, Vol. 7342). Springer, 1\u20136."},{"key":"e_1_2_1_13_1","volume-title":"Gilles Barthe, Joost-Pieter Katoen","unstructured":"2020. Foundations of Probabilistic Programming , Gilles Barthe, Joost-Pieter Katoen , and Alexandra Silva (Eds.). Cambridge University Press . 2020. Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva (Eds.). Cambridge University Press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_2_1_15_1","volume-title":"Smolka","author":"Bartocci Ezio","year":"2011","unstructured":"Ezio Bartocci , Radu Grosu , Panagiotis Katsaros , C. R. Ramakrishnan , and Scott A . Smolka . 2011 . Model Repair for Probabilistic Systems. In TACAS (LNCS , Vol. 6605). Springer, 326\u2013 340 . Ezio Bartocci, Radu Grosu, Panagiotis Katsaros, C. R. Ramakrishnan, and Scott A. Smolka. 2011. Model Repair for Probabilistic Systems. In TACAS (LNCS, Vol. 6605). Springer, 326\u2013340."},{"key":"e_1_2_1_16_1","volume-title":"ATVA (LNCS","volume":"276","author":"Bartocci Ezio","year":"2019","unstructured":"Ezio Bartocci , Laura Kov\u00e1cs , and Miroslav Stankovic . 2019 . Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops . In ATVA (LNCS , Vol. 11781). Springer, 255\u2013 276 . Ezio Bartocci, Laura Kov\u00e1cs, and Miroslav Stankovic. 2019. Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In ATVA (LNCS, Vol. 11781). Springer, 255\u2013276."},{"key":"e_1_2_1_17_1","volume-title":"Joost-Pieter Katoen, and Christoph Matheja.","author":"Batz Kevin","year":"2023","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. To appear 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. To appear"},{"key":"e_1_2_1_18_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Philipp Schr\u00f6er.","author":"Batz Kevin","year":"2021","unstructured":"Kevin Batz , Mingshuai Chen , Benjamin Lucien Kaminski , Joost-Pieter Katoen, Christoph Matheja, and Philipp Schr\u00f6er. 2021 . Latticed k-Induction with an Application to Probabilistic Programs. In CAV (I) (LNCS , Vol. 12760). Springer, 524\u2013 549 . Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Philipp Schr\u00f6er. 2021. Latticed k-Induction with an Application to Probabilistic Programs. In CAV (I) (LNCS, Vol. 12760). Springer, 524\u2013549."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/1909829"},{"key":"e_1_2_1_22_1","volume-title":"Vaandrager","author":"Bohnenkamp Henrik C.","year":"2003","unstructured":"Henrik C. Bohnenkamp , Peter van der Stok , Holger Hermanns , and Frits W . Vaandrager . 2003 . Cost-Optimization of the IPv4 Zeroconf Protocol. In DSN. IEEE Computer Society , 531\u2013540. Henrik C. Bohnenkamp, Peter van der Stok, Holger Hermanns, and Frits W. Vaandrager. 2003. Cost-Optimization of the IPv4 Zeroconf Protocol. In DSN. IEEE Computer Society, 531\u2013540."},{"key":"e_1_2_1_23_1","volume-title":"ATVA (LNCS","volume":"114","author":"Br\u00e1zdil Tom\u00e1s","year":"2014","unstructured":"Tom\u00e1s Br\u00e1zdil , Krishnendu Chatterjee , Martin Chmelik , Vojtech Forejt , Jan Kret\u00ednsk\u00fd , Marta Z. Kwiatkowska , David Parker , and Mateusz Ujma . 2014 . Verification of Markov Decision Processes Using Learning Algorithms . In ATVA (LNCS , Vol. 8837). Springer, 98\u2013 114 . Tom\u00e1s Br\u00e1zdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kret\u00ednsk\u00fd, Marta Z. Kwiatkowska, David Parker, and Mateusz Ujma. 2014. Verification of Markov Decision Processes Using Learning Algorithms. In ATVA (LNCS, Vol. 8837). Springer, 98\u2013114."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2958738"},{"key":"e_1_2_1_25_1","volume-title":"CAV (LNCS","volume":"526","author":"Chakarov Aleksandar","year":"2013","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan . 2013 . Probabilistic Program Analysis with Martingales . In CAV (LNCS , Vol. 8044). Springer, 511\u2013 526 . Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV (LNCS, Vol. 8044). Springer, 511\u2013526."},{"key":"e_1_2_1_26_1","volume-title":"SAS (LNCS","volume":"100","author":"Chakarov Aleksandar","year":"2014","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan . 2014 . Expectation Invariants for Probabilistic Program Loops as Fixed Points . In SAS (LNCS , Vol. 8723). Springer, 85\u2013 100 . Aleksandar Chakarov and Sriram Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In SAS (LNCS, Vol. 8723). Springer, 85\u2013100."},{"key":"e_1_2_1_27_1","volume-title":"CAV (I) (LNCS","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Amir Kafshdar Goharshady . 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s . In CAV (I) (LNCS , Vol. 9779). Springer, 3\u2013 22 . Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In CAV (I) (LNCS, Vol. 9779). Springer, 3\u201322."},{"key":"e_1_2_1_28_1","volume-title":"Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Petr Novotn\u00fd . 2020. Termination Analysis of Probabilistic Programs with Martingales . In Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen , and Alexandra Silva (Eds.). Cambridge University Press , 221\u2013258. Krishnendu Chatterjee, Hongfei Fu, and Petr Novotn\u00fd. 2020. Termination Analysis of Probabilistic Programs with Martingales. In Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva (Eds.). Cambridge University Press, 221\u2013258."},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In POPL. ACM 327\u2013342. \t\t\t\t  Krishnendu Chatterjee Hongfei Fu Petr Novotn\u00fd and Rouzbeh Hasheminezhad. 2016. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. In POPL. ACM 327\u2013342.","DOI":"10.1145\/2914770.2837639"},{"key":"e_1_2_1_30_1","volume-title":"Tobias Meggendorfer, and Djordje Zikelic.","author":"Chatterjee Krishnendu","year":"2022","unstructured":"Krishnendu Chatterjee , Amir Kafshdar Goharshady , Tobias Meggendorfer, and Djordje Zikelic. 2022 . Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. In CAV (I) (LNCS , Vol. 13371). Springer, 55\u2013 78 . Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Djordje Zikelic. 2022. Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. In CAV (I) (LNCS, Vol. 13371). Springer, 55\u201378."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and Dorde Zikelic. 2017. Stochastic Invariants for Probabilistic Termination. In POPL. ACM 145\u2013160. \t\t\t\t  Krishnendu Chatterjee Petr Novotn\u00fd and Dorde Zikelic. 2017. Stochastic Invariants for Probabilistic Termination. In POPL. ACM 145\u2013160.","DOI":"10.1145\/3093333.3009873"},{"key":"e_1_2_1_32_1","volume-title":"CAV (I) (LNCS","author":"Chen Mingshuai","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 (I) (LNCS , Vol. 13371). Springer, 79\u2013 101 . 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 (I) (LNCS, Vol. 13371). Springer, 79\u2013101."},{"key":"e_1_2_1_33_1","volume-title":"CAV (I) (LNCS","author":"Chen Yu-Fang","unstructured":"Yu-Fang Chen , Chih-Duo Hong , Bow-Yaw Wang , and Lijun Zhang . 2015. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation . In CAV (I) (LNCS , Vol. 9206). Springer, 658\u2013 674 . Yu-Fang Chen, Chih-Duo Hong, Bow-Yaw Wang, and Lijun Zhang. 2015. Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. In CAV (I) (LNCS, Vol. 9206). Springer, 658\u2013674."},{"key":"e_1_2_1_34_1","volume-title":"Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen","author":"Dahlqvist Fredrik","unstructured":"Fredrik Dahlqvist , Alexandra Silva , and Dexter Kozen . 2020. Semantics of Probabilistic Programming: A Gentle Introduction . In Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen , and Alexandra Silva (Eds.). Cambridge University Press , 1\u201342. Fredrik Dahlqvist, Alexandra Silva, and Dexter Kozen. 2020. Semantics of Probabilistic Programming: A Gentle Introduction. In Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva (Eds.). Cambridge University Press, 1\u201342."},{"key":"e_1_2_1_35_1","volume-title":"CAV (II) (LNCS","volume":"600","author":"Dehnert Christian","year":"2017","unstructured":"Christian Dehnert , Sebastian Junges , Joost-Pieter Katoen , and Matthias Volk . 2017 . A Storm is Coming: A Modern Probabilistic Model Checker . In CAV (II) (LNCS , Vol. 10427). Springer, 592\u2013 600 . Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. 2017. A Storm is Coming: A Modern Probabilistic Model Checker. In CAV (II) (LNCS, Vol. 10427). Springer, 592\u2013600."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_37_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","unstructured":"Edsger Wybe Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_2_1_38_1","unstructured":"Owain Evans Andreas Stuhlm\u00fcller John Salvatier and Daniel Filan. 2017. Modeling Agents with Probabilistic Programs. http:\/\/agentmodels.org Accessed: 2022-7-7 \t\t\t\t  Owain Evans Andreas Stuhlm\u00fcller John Salvatier and Daniel Filan. 2017. Modeling Agents with Probabilistic Programs. http:\/\/agentmodels.org Accessed: 2022-7-7"},{"key":"e_1_2_1_39_1","volume-title":"An Introduction to Probability Theory and Its Applications. I","author":"Feller Willliam","unstructured":"Willliam Feller . 1950. An Introduction to Probability Theory and Its Applications. I , John Wiley & Sons . Willliam Feller. 1950. An Introduction to Probability Theory and Its Applications. I, John Wiley & Sons."},{"key":"e_1_2_1_40_1","volume-title":"Joost-Pieter Katoen, and Naijun Zhan.","author":"Feng Shenghua","year":"2023","unstructured":"Shenghua Feng , Mingshuai Chen , Han Su , Benjamin Lucien Kaminski , Joost-Pieter Katoen, and Naijun Zhan. 2023 . Lower Bounds for Possibly Divergent Probabilistic Programs. CoRR , abs\/2302.06082 (2023), arXiv:2302.06082. Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Naijun Zhan. 2023. Lower Bounds for Possibly Divergent Probabilistic Programs. CoRR, abs\/2302.06082 (2023), arXiv:2302.06082."},{"key":"e_1_2_1_41_1","volume-title":"ATVA (LNCS","volume":"416","author":"Feng Yijun","year":"2017","unstructured":"Yijun Feng , Lijun Zhang , David N. Jansen , Naijun Zhan , and Bican Xia . 2017 . Finding Polynomial Loop Invariants for Probabilistic Programs . In ATVA (LNCS , Vol. 10482). Springer, 400\u2013 416 . Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, and Bican Xia. 2017. Finding Polynomial Loop Invariants for Probabilistic Programs. In ATVA (LNCS, Vol. 10482). Springer, 400\u2013416."},{"key":"e_1_2_1_42_1","volume-title":"Probabilistic Termination: Soundness, Completeness, and Compositionality. In POPL. ACM, 489\u2013501.","author":"Ferrer Fioriti Luis Mar\u00eda","year":"2015","unstructured":"Luis Mar\u00eda Ferrer Fioriti and Holger Hermanns . 2015 . Probabilistic Termination: Soundness, Completeness, and Compositionality. In POPL. ACM, 489\u2013501. Luis Mar\u00eda Ferrer Fioriti and Holger Hermanns. 2015. Probabilistic Termination: Soundness, Completeness, and Compositionality. In POPL. ACM, 489\u2013501."},{"key":"e_1_2_1_43_1","article-title":"Inferring Lower Runtime Bounds for Integer Programs","volume":"42","author":"Frohn Florian","year":"2020","unstructured":"Florian Frohn , Matthias Naaf , Marc Brockschmidt , and J\u00fcrgen Giesl . 2020 . Inferring Lower Runtime Bounds for Integer Programs . ACM Trans. Program. Lang. Syst. , 42 , 3 (2020), 13:1\u201313:50. Florian Frohn, Matthias Naaf, Marc Brockschmidt, and J\u00fcrgen Giesl. 2020. Inferring Lower Runtime Bounds for Integer Programs. ACM Trans. Program. Lang. Syst., 42, 3 (2020), 13:1\u201313:50.","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"e_1_2_1_44_1","volume-title":"IJCAR (LNCS","volume":"567","author":"Frohn Florian","year":"2016","unstructured":"Florian Frohn , Matthias Naaf , Jera Hensel , Marc Brockschmidt , and J\u00fcrgen Giesl . 2016 . Lower Runtime Bounds for Integer Programs . In IJCAR (LNCS , Vol. 9706). Springer, 550\u2013 567 . Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, and J\u00fcrgen Giesl. 2016. Lower Runtime Bounds for Integer Programs. In IJCAR (LNCS, Vol. 9706). Springer, 550\u2013567."},{"key":"e_1_2_1_45_1","volume-title":"VMCAI (LNCS","volume":"490","author":"Fu Hongfei","year":"2019","unstructured":"Hongfei Fu and Krishnendu Chatterjee . 2019 . Termination of Nondeterministic Probabilistic Programs . In VMCAI (LNCS , Vol. 11388). Springer, 468\u2013 490 . Hongfei Fu and Krishnendu Chatterjee. 2019. Termination of Nondeterministic Probabilistic Programs. In VMCAI (LNCS, Vol. 11388). Springer, 468\u2013490."},{"key":"e_1_2_1_46_1","volume-title":"CADE (LNCS","volume":"286","author":"Giesl J\u00fcrgen","year":"2019","unstructured":"J\u00fcrgen Giesl , Peter Giesl , and Marcel Hark . 2019 . Computing Expected Runtimes for Constant Probability Programs . In CADE (LNCS , Vol. 11716). Springer, 269\u2013 286 . J\u00fcrgen Giesl, Peter Giesl, and Marcel Hark. 2019. Computing Expected Runtimes for Constant Probability Programs. In CADE (LNCS, Vol. 11716). Springer, 269\u2013286."},{"key":"e_1_2_1_47_1","volume-title":"Rajamani","author":"Gordon Andrew D.","year":"2014","unstructured":"Andrew D. Gordon , Thomas A. Henzinger , Aditya V. Nori , and Sriram K . Rajamani . 2014 . Probabilistic Programming. In FOSE. ACM , 167\u2013181. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic Programming. In FOSE. ACM, 167\u2013181."},{"key":"e_1_2_1_48_1","volume-title":"J\u00fcrgen Giesl, and Joost-Pieter Katoen.","author":"Hark Marcel","year":"2019","unstructured":"Marcel Hark , Benjamin Lucien Kaminski , J\u00fcrgen Giesl, and Joost-Pieter Katoen. 2019 . Aiming Low Is Harder \u2013 Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification. CoRR , abs\/1904.01117 (2019), arXiv:1904.01117. Marcel Hark, Benjamin Lucien Kaminski, J\u00fcrgen Giesl, and Joost-Pieter Katoen. 2019. Aiming Low Is Harder \u2013 Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification. CoRR, abs\/1904.01117 (2019), arXiv:1904.01117."},{"key":"e_1_2_1_49_1","volume-title":"Proc. ACM Program. Lang., 4, POPL","author":"Hark Marcel","year":"2020","unstructured":"Marcel Hark , Benjamin Lucien Kaminski , J\u00fcrgen Giesl , and Joost-Pieter Katoen . 2020 . Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification . Proc. ACM Program. Lang., 4, POPL (2020), 37:1\u201337:28. Marcel Hark, Benjamin Lucien Kaminski, J\u00fcrgen Giesl, and Joost-Pieter Katoen. 2020. Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification. Proc. ACM Program. Lang., 4, POPL (2020), 37:1\u201337:28."},{"key":"e_1_2_1_50_1","volume-title":"CAV (II) (LNCS","volume":"511","author":"Hartmanns Arnd","year":"2020","unstructured":"Arnd Hartmanns and Benjamin Lucien Kaminski . 2020 . Optimistic Value Iteration . In CAV (II) (LNCS , Vol. 12225). Springer, 488\u2013 511 . Arnd Hartmanns and Benjamin Lucien Kaminski. 2020. Optimistic Value Iteration. In CAV (II) (LNCS, Vol. 12225). Springer, 488\u2013511."},{"key":"e_1_2_1_51_1","volume-title":"TACAS (I) (LNCS","author":"Hartmanns Arnd","unstructured":"Arnd Hartmanns , Michaela Klauck , David Parker , Tim Quatmann , and Enno Ruijters . 2019. The Quantitative Verification Benchmark Set . In TACAS (I) (LNCS , Vol. 11427). Springer, 344\u2013 350 . Arnd Hartmanns, Michaela Klauck, David Parker, Tim Quatmann, and Enno Ruijters. 2019. The Quantitative Verification Benchmark Set. In TACAS (I) (LNCS, Vol. 11427). Springer, 344\u2013350."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0157-0"},{"key":"e_1_2_1_53_1","unstructured":"Michael Hicks. 2014. What is Probabilistic Programming? In: The Programming Languages Enthusiast. http:\/\/www.pl-enthusiast.net\/2014\/09\/08 Accessed: 2021-12-09 \t\t\t\t  Michael Hicks. 2014. What is Probabilistic Programming? In: The Programming Languages Enthusiast. http:\/\/www.pl-enthusiast.net\/2014\/09\/08 Accessed: 2021-12-09"},{"key":"e_1_2_1_54_1","volume-title":"CAV (I) (LNCS","author":"Hong Chih-Duo","unstructured":"Chih-Duo Hong , Anthony W. Lin , Rupak Majumdar , and Philipp R\u00fcmmer . 2019. Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols) . In CAV (I) (LNCS , Vol. 11561). Springer, 455\u2013 474 . Chih-Duo Hong, Anthony W. Lin, Rupak Majumdar, and Philipp R\u00fcmmer. 2019. Probabilistic Bisimulation for Parameterized Systems - (with Applications to Verifying Anonymous Protocols). In CAV (I) (LNCS, Vol. 11561). Springer, 455\u2013474."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700022243"},{"key":"e_1_2_1_56_1","volume-title":"Joost-Pieter Katoen, and Lukas Westhofen.","author":"Jansen Nils","year":"2016","unstructured":"Nils Jansen , Christian Dehnert , Benjamin Lucien Kaminski , Joost-Pieter Katoen, and Lukas Westhofen. 2016 . Bounded Model Checking for Probabilistic Programs. In ATVA (LNCS , Vol. 9938). 68\u2013 85 . Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen. 2016. Bounded Model Checking for Probabilistic Programs. In ATVA (LNCS, Vol. 9938). 68\u201385."},{"key":"e_1_2_1_57_1","unstructured":"Claire Jones. 1990. Probabilistic Non-determinism. Ph. D. Dissertation. University of Edinburgh UK. \t\t\t\t  Claire Jones. 1990. Probabilistic Non-determinism. Ph. D. Dissertation. University of Edinburgh UK."},{"key":"e_1_2_1_58_1","volume-title":"Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph. D. Dissertation","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski . 2019. Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph. D. Dissertation . RWTH Aachen University , Germany . Benjamin Lucien Kaminski. 2019. Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph. D. Dissertation. RWTH Aachen University, Germany."},{"key":"e_1_2_1_59_1","volume-title":"A Weakest Pre-expectation Semantics for Mixed-Sign Expectations","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen . 2017. A Weakest Pre-expectation Semantics for Mixed-Sign Expectations . In LICS. IEEE Computer Society , 1\u201312. Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2017. A Weakest Pre-expectation Semantics for Mixed-Sign Expectations. In LICS. IEEE Computer Society, 1\u201312."},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_1_61_1","volume-title":"ESOP (LNCS","volume":"389","author":"Kaminski Benjamin Lucien","year":"2016","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 (LNCS , Vol. 9632). Springer, 364\u2013 389 . Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In ESOP (LNCS, Vol. 9632). Springer, 364\u2013389."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_63_1","doi-asserted-by":"crossref","unstructured":"Joost-Pieter Katoen. 2016. The Probabilistic Model Checking Landscape. In LICS. ACM 31\u201345. \t\t\t\t  Joost-Pieter Katoen. 2016. The Probabilistic Model Checking Landscape. In LICS. ACM 31\u201345.","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_2_1_64_1","volume-title":"Benjamin Lucien Kaminski, and Federico Olmedo","author":"Katoen Joost-Pieter","year":"2015","unstructured":"Joost-Pieter Katoen , Friedrich Gretz , Nils Jansen , Benjamin Lucien Kaminski, and Federico Olmedo . 2015 . Understanding Probabilistic Programs. In Correct System Design (LNCS , Vol. 9360). Springer, 15\u2013 32 . Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, and Federico Olmedo. 2015. Understanding Probabilistic Programs. In Correct System Design (LNCS, Vol. 9360). Springer, 15\u201332."},{"key":"e_1_2_1_65_1","volume-title":"Morgan","author":"Katoen Joost-Pieter","year":"2010","unstructured":"Joost-Pieter Katoen , Annabelle McIver , Larissa Meinicke , and Carroll C . Morgan . 2010 . Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. In SAS (LNCS , Vol. 6337). Springer, 390\u2013 406 . Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. In SAS (LNCS, Vol. 6337). Springer, 390\u2013406."},{"key":"e_1_2_1_66_1","first-page":"133","article-title":"Un Th\u00e9or\u00e8me sur les Functions D\u2019ensembles","volume":"6","author":"Knaster Bronis\u0142","year":"1928","unstructured":"Bronis\u0142 aw Knaster . 1928 . Un Th\u00e9or\u00e8me sur les Functions D\u2019ensembles . Annales de la Societe Polonaise de Mathematique , 6 (1928), 133 \u2013 134 . Bronis\u0142 aw Knaster. 1928. Un Th\u00e9or\u00e8me sur les Functions D\u2019ensembles. Annales de la Societe Polonaise de Mathematique, 6 (1928), 133\u2013134.","journal-title":"Annales de la Societe Polonaise de Mathematique"},{"key":"e_1_2_1_67_1","volume-title":"Ugo Dal Lago, and Charles Grellois","author":"Kobayashi Naoki","year":"2020","unstructured":"Naoki Kobayashi , Ugo Dal Lago, and Charles Grellois . 2020 . On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci ., 16, 4 (2020). Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2020. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. Log. Methods Comput. Sci., 16, 4 (2020)."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_69_1","doi-asserted-by":"crossref","unstructured":"Dexter Kozen. 1983. A Probabilistic PDL. In STOC. ACM 291\u2013297. \t\t\t\t  Dexter Kozen. 1983. A Probabilistic PDL. In STOC. ACM 291\u2013297.","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_71_1","volume-title":"PRISM: Probabilistic Symbolic Model Checker","author":"Kwiatkowska Marta","year":"2002","unstructured":"Marta Kwiatkowska , Gethin Norman , and David Parker . 2002 . PRISM: Probabilistic Symbolic Model Checker . In TOOLS. Springer , 200\u2013204. Marta Kwiatkowska, Gethin Norman, and David Parker. 2002. PRISM: Probabilistic Symbolic Model Checker. In TOOLS. Springer, 200\u2013204."},{"key":"e_1_2_1_72_1","volume-title":"Model Checking for Probability and Time: From Theory to Practice","author":"Kwiatkowska Marta Z.","unstructured":"Marta Z. Kwiatkowska . 2003. Model Checking for Probability and Time: From Theory to Practice . In LICS. IEEE Computer Society , 351. Marta Z. Kwiatkowska. 2003. Model Checking for Probability and Time: From Theory to Practice. In LICS. IEEE Computer Society, 351."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(82)90065-5"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0370164600020265"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00208-5"},{"key":"e_1_2_1_77_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_78_1","volume-title":"Proc. ACM Program. Lang., 2, POPL","author":"McIver Annabelle","year":"2018","unstructured":"Annabelle McIver , Carroll Morgan , Benjamin Lucien Kaminski , and Joost-Pieter Katoen . 2018 . A New Proof Rule for Almost-Sure Termination . Proc. ACM Program. Lang., 2, POPL (2018), 33:1\u201333:28. Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. 2018. A New Proof Rule for Almost-Sure Termination. Proc. ACM Program. Lang., 2, POPL (2018), 33:1\u201333:28."},{"key":"e_1_2_1_79_1","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1137\/0104014","article-title":"Random Walks in Multidimensional Spaces, Especially on Periodic Lattices","volume":"4","author":"Montroll Elliot W","year":"1956","unstructured":"Elliot W Montroll . 1956 . Random Walks in Multidimensional Spaces, Especially on Periodic Lattices . J. Soc. Indust. Appl. Math. , 4 , 4 (1956), 241 \u2013 260 . Elliot W Montroll. 1956. Random Walks in Multidimensional Spaces, Especially on Periodic Lattices. J. Soc. Indust. Appl. Math., 4, 4 (1956), 241\u2013260.","journal-title":"J. Soc. Indust. Appl. Math."},{"key":"e_1_2_1_80_1","volume-title":"FM (LNCS","volume":"675","author":"Moosbrugger Marcel","year":"2021","unstructured":"Marcel Moosbrugger , Ezio Bartocci , Joost-Pieter Katoen , and Laura Kov\u00e1cs . 2021 . The Probabilistic Termination Tool Amber . In FM (LNCS , Vol. 13047). Springer, 667\u2013 675 . Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kov\u00e1cs. 2021. The Probabilistic Termination Tool Amber. In FM (LNCS, Vol. 13047). Springer, 667\u2013675."},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/7.6.779"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_83_1","volume-title":"Murawski and Jo\u00ebl Ouaknine","author":"Andrzej","year":"2005","unstructured":"Andrzej S. Murawski and Jo\u00ebl Ouaknine . 2005 . On Probabilistic Program Equivalence and Refinement. In CONCUR (LNCS , Vol. 3653). Springer, 156\u2013 170 . Andrzej S. Murawski and Jo\u00ebl Ouaknine. 2005. On Probabilistic Program Equivalence and Refinement. In CONCUR (LNCS, Vol. 3653). Springer, 156\u2013170."},{"key":"e_1_2_1_84_1","volume-title":"Bounded Expectations: Resource Analysis for Probabilistic Programs. In PLDI. ACM, 496\u2013512.","author":"Ngo Van Chan","year":"2018","unstructured":"Van Chan Ngo , Quentin Carbonneaux , and Jan Hoffmann . 2018 . Bounded Expectations: Resource Analysis for Probabilistic Programs. In PLDI. ACM, 496\u2013512. Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. 2018. Bounded Expectations: Resource Analysis for Probabilistic Programs. In PLDI. ACM, 496\u2013512."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_86_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. ACM , 672\u2013681. Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about Recursive Probabilistic Programs. In LICS. ACM, 672\u2013681."},{"key":"e_1_2_1_87_1","volume-title":"Fixpoint Induction and Proofs of Program Properties. Machine Intelligence, 5","author":"Park David","year":"1969","unstructured":"David Park . 1969. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence, 5 ( 1969 ). David Park. 1969. Fixpoint Induction and Proofs of Program Properties. Machine Intelligence, 5 (1969)."},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01458701"},{"key":"e_1_2_1_89_1","volume-title":"CAV (I) (LNCS","author":"Quatmann Tim","unstructured":"Tim Quatmann and Joost-Pieter Katoen . 2018. Sound Value Iteration . In CAV (I) (LNCS , Vol. 10981). Springer, 643\u2013 661 . Tim Quatmann and Joost-Pieter Katoen. 2018. Sound Value Iteration. In CAV (I) (LNCS, Vol. 10981). Springer, 643\u2013661."},{"key":"e_1_2_1_90_1","volume-title":"MFCS (LNCS","volume":"451","author":"Saheb-Djahromi Nasser","year":"1978","unstructured":"Nasser Saheb-Djahromi . 1978 . Probabilistic LCF . In MFCS (LNCS , Vol. 64). Springer, 442\u2013 451 . Nasser Saheb-Djahromi. 1978. Probabilistic LCF. In MFCS (LNCS, Vol. 64). Springer, 442\u2013451."},{"key":"e_1_2_1_91_1","volume-title":"Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen","author":"Sankaranarayanan Sriram","unstructured":"Sriram Sankaranarayanan . 2020. Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities . In Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen , and Alexandra Silva (Eds.). Cambridge University Press , 259\u2013294. Sriram Sankaranarayanan. 2020. Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities. In Foundations of Probabilistic Programming, Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva (Eds.). Cambridge University Press, 259\u2013294."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/151254.151256"},{"key":"e_1_2_1_93_1","volume-title":"Marco Gaboardi, and Nils Napp.","author":"Shamsi Seyed Mahdi","year":"2020","unstructured":"Seyed Mahdi Shamsi , Gian Pietro Farina , Marco Gaboardi, and Nils Napp. 2020 . Probabilistic Programming Languages for Modeling Autonomous Systems. In MFI. IEEE , 32\u201339. Seyed Mahdi Shamsi, Gian Pietro Farina, Marco Gaboardi, and Nils Napp. 2020. Probabilistic Programming Languages for Modeling Autonomous Systems. In MFI. IEEE, 32\u201339."},{"key":"e_1_2_1_94_1","volume-title":"Continuous Distributions and Divergence. In SETSS (LNCS","volume":"121","author":"Szymczak Marcin","year":"2019","unstructured":"Marcin Szymczak and Joost-Pieter Katoen . 2019 . Weakest Preexpectation Semantics for Bayesian Inference - Conditioning , Continuous Distributions and Divergence. In SETSS (LNCS , Vol. 12154). Springer, 44\u2013 121 . Marcin Szymczak and Joost-Pieter Katoen. 2019. Weakest Preexpectation Semantics for Bayesian Inference - Conditioning, Continuous Distributions and Divergence. In SETSS (LNCS, Vol. 12154). Springer, 44\u2013121."},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_96_1","volume-title":"An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756","author":"van de Meent Jan-Willem","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 ). Jan-Willem van de Meent, Brooks Paige, Hongseok Yang, and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756 (2018)."},{"key":"e_1_2_1_97_1","volume-title":"Reps","author":"Wang Di","year":"2021","unstructured":"Di Wang , Jan Hoffmann , and Thomas W . Reps . 2021 . Central Moment Analysis for Cost Accumulators in Probabilistic Programs. In PLDI. ACM , 559\u2013573. Di Wang, Jan Hoffmann, and Thomas W. Reps. 2021. Central Moment Analysis for Cost Accumulators in Probabilistic Programs. In PLDI. ACM, 559\u2013573."},{"key":"e_1_2_1_98_1","doi-asserted-by":"crossref","unstructured":"Jinyi Wang Yican Sun Hongfei Fu Krishnendu Chatterjee and Amir Kafshdar Goharshady. 2021. Quantitative Analysis of Assertion Violations in Probabilistic Programs. In PLDI. ACM 1171\u20131186. \t\t\t\t  Jinyi Wang Yican Sun Hongfei Fu Krishnendu Chatterjee and Amir Kafshdar Goharshady. 2021. Quantitative Analysis of Assertion Violations in Probabilistic Programs. In PLDI. ACM 1171\u20131186.","DOI":"10.1145\/3410310"},{"key":"e_1_2_1_99_1","volume-title":"Proc. ACM Program. Lang., 4, POPL","author":"Wang Peixin","year":"2020","unstructured":"Peixin Wang , Hongfei Fu , Krishnendu Chatterjee , Yuxin Deng , and Ming Xu . 2020 . Proving Expected Sensitivity of Probabilistic Programs With Randomized Variable-Dependent Termination Time . Proc. ACM Program. Lang., 4, POPL (2020), 25:1\u201325:30. Peixin Wang, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. 2020. Proving Expected Sensitivity of Probabilistic Programs With Randomized Variable-Dependent Termination Time. Proc. ACM Program. Lang., 4, POPL (2020), 25:1\u201325:30."},{"key":"e_1_2_1_100_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. ACM , 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. ACM, 204\u2013220."},{"key":"e_1_2_1_101_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."},{"key":"e_1_2_1_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586051","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586051","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:10Z","timestamp":1750183690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586051"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":102,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586051"],"URL":"https:\/\/doi.org\/10.1145\/3586051","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}