{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:22Z","timestamp":1780994482843,"version":"3.54.1"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["2236"],"award-info":[{"award-number":["2236"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["787914"],"award-info":[{"award-number":["787914"]}],"id":[{"id":"10.13039\/100011199","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":[[2020,1]]},"abstract":"<jats:p>We present a new inductive rule for verifying lower bounds on expected values of random variables after execution of probabilistic loops as well as on their expected runtimes. Our rule is<jats:italic>simple<\/jats:italic>in the sense that loop body semantics need to be applied only finitely often in order to verify that the candidates are indeed lower bounds. In particular, it is not necessary to find the limit of a sequence as in many previous rules.<\/jats:p>","DOI":"10.1145\/3371105","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Aiming low is harder: induction for lower bounds in probabilistic program verification"],"prefix":"10.1145","volume":"4","author":[{"given":"Marcel","family":"Hark","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_2_3_1","volume-title":"Refinement Calculus - A Systematic Introduction","author":"Back Ralph-Johan"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(91)90413-V"},{"key":"e_1_2_2_5_1","volume-title":"Decomposition. In Proc. of the International Conference on Computer\u2013Aided Verification (CAV) (Lecture Notes in Computer Science)","volume":"9779","author":"Barthe Gilles","year":"2016"},{"key":"e_1_2_2_6_1","volume-title":"Joost-Pieter Katoen, Christoph Matheja, and Thomas Noll.","author":"Batz Kevin","year":"2019"},{"key":"e_1_2_2_7_1","volume-title":"Proc. of the European Symposium on Programming Languages and Systems (ESOP) (Lecture Notes in Computer Science)","volume":"10801","author":"Batz Kevin","year":"2018"},{"key":"e_1_2_2_8_1","volume-title":"Probability Theory and Elements of Measure Theory (first english ed.). Holt, Rinehart and Winston","author":"Bauer Heinz"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"e_1_2_2_14_1","volume-title":"pGCL for Isabelle. Archive of Formal Proofs","author":"Cock David","year":"2014"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_16_1","unstructured":"Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice\u2013Hall. Edsger Wybe Dijkstra. 1976. A Discipline of Programming. Prentice\u2013Hall."},{"key":"e_1_2_2_17_1","volume-title":"An Introduction to Probability Theory and its Applications","author":"Feller William"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_37"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_2_22_1","volume-title":"Probabilistic Programming. In Proc. of Future of Software Engineering (FOSE). ACM, 167\u2013181","author":"Gordon Andrew D."},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","volume-title":"Probability and Random Processes","author":"Grimmett Geoffrey","DOI":"10.1093\/oso\/9780198572237.001.0001"},{"key":"e_1_2_2_24_1","volume-title":"J\u00fcrgen Giesl, and Joost-Pieter Katoen.","author":"Hark Marcel","year":"2019"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0157-0"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935319"},{"key":"e_1_2_2_27_1","volume-title":"New Approaches for Almost\u2013Sure Termination of Probabilistic Programs (Lecture Notes in Computer Science)","author":"Huang Mingzhang"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700022243"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_5"},{"key":"e_1_2_2_30_1","unstructured":"Claire Jones. 1990. Probabilistic Non\u2013Determinism. Ph.D. Dissertation. University of Edinburgh UK. Claire Jones. 1990. Probabilistic Non\u2013Determinism. Ph.D. Dissertation. University of Edinburgh UK."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_35_1","volume-title":"Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. Journal of the ACM 65","author":"Kaminski Benjamin Lucien","year":"2018"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.016"},{"key":"e_1_2_2_38_1","volume-title":"Ugo Dal Lago, and Charles Grellois","author":"Kobayashi Naoki","year":"2018"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(82)90065-5"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00208-5"},{"key":"e_1_2_2_43_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.008"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.14236\/ewic\/RW1996.10"},{"key":"e_1_2_2_46_1","first-page":"779","article-title":"An Expectation\u2013Transformer Model for Probabilistic Temporal Logic","volume":"7","author":"Morgan Carroll","year":"1999","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_48_1","volume-title":"Randomized Algorithms","author":"Motwani Rajeev"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_2_52_1","volume-title":"Fixpoint Induction and Proofs of Program Properties. Machine Intelligence 5","author":"Park David","year":"1969"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1002\/zamm.19300100113"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371105","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371105","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371105"],"URL":"https:\/\/doi.org\/10.1145\/3371105","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}