{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:53Z","timestamp":1775868473607,"version":"3.50.1"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T00:00:00Z","timestamp":1535500800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Excellence Initiative of the German federal and state government"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2018,10,31]]},"abstract":"<jats:p>This article presents a wp--style calculus for obtaining bounds on the expected runtime of randomized algorithms. Its application includes determining the (possibly infinite) expected termination time of a randomized algorithm and proving positive almost--sure termination\u2014does a program terminate with probability one in finite expected time? We provide several proof rules for bounding the runtime of loops, and prove the soundness of the approach with respect to a simple operational model. We show that our approach is a conservative extension of Nielson\u2019s approach for reasoning about the runtime of deterministic programs. We analyze the expected runtime of some example programs including the coupon collector\u2019s problem, a one--dimensional random walk and a randomized binary search.<\/jats:p>","DOI":"10.1145\/3208102","type":"journal-article","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T13:45:11Z","timestamp":1535636711000},"page":"1-68","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":68,"title":["Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms"],"prefix":"10.1145","volume":"65","author":[{"given":"Benjamin Lucien","family":"Kaminski","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"given":"Federico","family":"Olmedo","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Chile, Santiago, Chile"}]}],"member":"320","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614438"},{"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":"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 Computer-Aided Verification (CAV\u201916) (LNCS), Vol. 9779 . Springer , 43--61. Gilles Barthe, Thomas Espitau, Luis Mar\u00eda Ferrer Fioriti, and Justin Hsu. 2016. Synthesizing probabilistic invariants via doob\u2019s decomposition. In Computer-Aided Verification (CAV\u201916) (LNCS), Vol. 9779. Springer, 43--61."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_7"},{"key":"e_1_2_1_5_1","volume-title":"Logic Based Program Synthesis and Transformation (LOPSTR\u201904) (LNCS)","author":"Berghammer Rudolf","unstructured":"Rudolf Berghammer and Markus M\u00fcller-Olm . 2004. Formal development and verification of approximation algorithms using auxiliary variables . In Logic Based Program Synthesis and Transformation (LOPSTR\u201904) (LNCS) , Vol. 3018 . Springer , 59--74. Rudolf Berghammer and Markus M\u00fcller-Olm. 2004. Formal development and verification of approximation algorithms using auxiliary variables. In Logic Based Program Synthesis and Transformation (LOPSTR\u201904) (LNCS), Vol. 3018. Springer, 59--74."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0166-0"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.06.005"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11526841_9"},{"key":"e_1_2_1_9_1","volume-title":"Computer Aided Verification (CAV\u201913) (LNCS)","author":"Chakarov Aleksandar","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan . 2013. Probabilistic program analysis with martingales . In Computer Aided Verification (CAV\u201913) (LNCS) , Vol. 8044 . Springer , 511--526. Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In Computer Aided Verification (CAV\u201913) (LNCS), Vol. 8044. Springer, 511--526."},{"key":"e_1_2_1_10_1","volume-title":"Computer-Aided Verification (CAV\u201917) (LNCS)","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee , Hongfei Fu , and Aniket Murhekar . 2017. Automated recurrence analysis for almost-linear expected-runtime bounds . In Computer-Aided Verification (CAV\u201917) (LNCS) , Vol. 10426 . Springer , 118--139. Krishnendu Chatterjee, Hongfei Fu, and Aniket Murhekar. 2017. Automated recurrence analysis for almost-linear expected-runtime bounds. In Computer-Aided Verification (CAV\u201917) (LNCS), Vol. 10426. Springer, 118--139."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_9"},{"key":"e_1_2_1_12_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edgser W.","unstructured":"Edgser W. Dijkstra . 1976. A Discipline of Programming . Prentice Hall . Edgser W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall."},{"key":"e_1_2_1_13_1","volume-title":"Automated Technology for Verification and Analysis (ATVA\u201917) (LNCS)","author":"Feng Yijun","unstructured":"Yijun Feng , Lijun Zhang , David N. Jansen , Naijun Zhan , and Bican Xia . 2017. Finding polynomial loop invariants for probabilistic programs . In Automated Technology for Verification and Analysis (ATVA\u201917) (LNCS) , Vol. 10482 . Springer , 400--416. Yijun Feng, Lijun Zhang, David N. Jansen, Naijun Zhan, and Bican Xia. 2017. Finding polynomial loop invariants for probabilistic programs. In Automated Technology for Verification and Analysis (ATVA\u201917) (LNCS), Vol. 10482. Springer, 400--416."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_15_1","volume-title":"Randomised Algorithms. Lecture Notes","author":"Frandsen Gudmund S.","unstructured":"Gudmund S. Frandsen . 1998. Randomised Algorithms. Lecture Notes , University of Aarhus , Denmark. Gudmund S. Frandsen. 1998. Randomised Algorithms. Lecture Notes, University of Aarhus, Denmark."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050017"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0157-0"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211249"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/42267.42275"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2362389.2362393"},{"key":"e_1_2_1_23_1","volume-title":"Interactive Theorem Proving (ITP\u201916) (LNCS)","author":"H\u00f6lzl Johannes","unstructured":"Johannes H\u00f6lzl . 2016. Formalising semantics for expected running time of probabilistic programs . In Interactive Theorem Proving (ITP\u201916) (LNCS) , Vol. 9807 . Springer , 475--482. Johannes H\u00f6lzl. 2016. Formalising semantics for expected running time of probabilistic programs. In Interactive Theorem Proving (ITP\u201916) (LNCS), Vol. 9807. Springer, 475--482."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.11.001"},{"key":"e_1_2_1_25_1","volume-title":"LNCS","volume":"2410","author":"Hurd Joe","year":"2002","unstructured":"Joe Hurd . 2002 . A formal approach to probabilistic termination. In Theorem Proving in Higher Order Logics (TPHOL\u201902) . LNCS , Vol. 2410 . Springer, 230--245. Joe Hurd. 2002. A formal approach to probabilistic termination. In Theorem Proving in Higher Order Logics (TPHOL\u201902). LNCS, Vol. 2410. Springer, 230--245."},{"key":"e_1_2_1_26_1","volume-title":"Elements of Random Walk and Diffusion Processes","author":"Ibe Oliver C.","unstructured":"Oliver C. Ibe . 2013. Elements of Random Walk and Diffusion Processes . John Wiley 8 Sons. Oliver C. Ibe. 2013. Elements of Random Walk and Diffusion Processes. John Wiley 8 Sons."},{"key":"e_1_2_1_27_1","volume-title":"Mathematical Foundations of Computer Science (MFCS\u201915), Part I (LNCS)","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen . 2015. On the hardness of almost-sure termination . In Mathematical Foundations of Computer Science (MFCS\u201915), Part I (LNCS) , Vol. 9234 . Springer , 307--318. Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2015. On the hardness of almost-sure termination. In Mathematical Foundations of Computer Science (MFCS\u201915), Part I (LNCS), Vol. 9234. Springer, 307--318."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/195613.195632"},{"key":"e_1_2_1_30_1","volume-title":"Static Analysis Symposium (SAS\u201910)","volume":"6337","author":"Katoen Joost-Pieter","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 Static Analysis Symposium (SAS\u201910) (LNCS), Vol. 6337 . Springer, 390--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 Static Analysis Symposium (SAS\u201910) (LNCS), Vol. 6337. Springer, 390--406."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-2(1:2)2006"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288637"},{"key":"e_1_2_1_35_1","volume-title":"Analysis of Algorithms -- An Active Learning Approach","author":"McConnell Jeffrey J.","unstructured":"Jeffrey J. McConnell . 2008. Analysis of Algorithms -- An Active Learning Approach . Jones and Bartlett Publishers . Jeffrey J. McConnell. 2008. Analysis of Algorithms -- An Active Learning Approach. Jones and Bartlett Publishers."},{"key":"e_1_2_1_36_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan . 2004. Abstraction , Refinement and Proof for Probabilistic Systems . Springer . Annabelle McIver and Carroll Morgan. 2004. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_37_1","volume-title":"Probability and Computing: Randomized Algorithms and Probabilistic Analysis","author":"Mitzenmacher Michael","unstructured":"Michael Mitzenmacher and Eli Upfal . 2005. Probability and Computing: Randomized Algorithms and Probabilistic Analysis . Cambridge University Press . Michael Mitzenmacher and Eli Upfal. 2005. Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647170.718306"},{"key":"e_1_2_1_39_1","volume-title":"Randomized Algorithms","author":"Motwani Rajeev","unstructured":"Rajeev Motwani and Prabhakar Raghavan . 1995. Randomized Algorithms . Cambridge University Press . Rajeev Motwani and Prabhakar Raghavan. 1995. Randomized Algorithms. Cambridge University Press."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90029-3"},{"key":"e_1_2_1_42_1","volume-title":"Semantics with Applications: An Appetizer","author":"Nielson Hanne Riis","unstructured":"Hanne Riis Nielson and Flemming Nielson . 2007. Semantics with Applications: An Appetizer . Springer . Hanne Riis Nielson and Flemming Nielson. 2007. Semantics with Applications: An Appetizer. Springer."},{"key":"e_1_2_1_43_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. CoRR abs\/1603.02922 (2016). Retrieved from http:\/\/arxiv.org\/abs\/1603.02922. Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about recursive probabilistic programs. CoRR abs\/1603.02922 (2016). Retrieved from http:\/\/arxiv.org\/abs\/1603.02922."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_45_1","volume-title":"Foundations of Mathematical Analysis","author":"Ponnusamy Saminathan","unstructured":"Saminathan Ponnusamy . 2011. Foundations of Mathematical Analysis . Springer Science 8 Business Media. Saminathan Ponnusamy. 2011. Foundations of Mathematical Analysis. Springer Science 8 Business Media."},{"key":"e_1_2_1_46_1","volume-title":"Handbook of Analysis and Its Foundations","author":"Schechter Eric","unstructured":"Eric Schechter . 1996. Handbook of Analysis and Its Foundations . Elsevier Science . Eric Schechter. 1996. Handbook of Analysis and Its Foundations. Elsevier Science."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S147106841400057X"},{"key":"e_1_2_1_48_1","volume-title":"Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science","author":"Wechler Wolfgang","unstructured":"Wolfgang Wechler . 1992. Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science , Vol. 25 . Springer . Wolfgang Wechler. 1992. Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science, Vol. 25. Springer."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1347375.1347389"},{"key":"e_1_2_1_50_1","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1993. The Formal Semantics of Programming Languages: An Introduction . MIT Press . Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3208102","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3208102","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:08:06Z","timestamp":1750212486000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3208102"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,29]]},"references-count":50,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,10,31]]}},"alternative-id":["10.1145\/3208102"],"URL":"https:\/\/doi.org\/10.1145\/3208102","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,29]]},"assertion":[{"value":"2017-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}