{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:47:31Z","timestamp":1775868451545,"version":"3.50.1"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["787914"],"award-info":[{"award-number":["787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DIREC","award":["AVSPPP"],"award-info":[{"award-number":["AVSPPP"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>This paper presents a quantitative program verification infrastructure for discrete  \nprobabilistic programs.  \nOur infrastructure can be viewed as the probabilistic analogue of Boogie:  \nits central components are an intermediate verification language (IVL) together with a real-valued logic.  \nOur IVL provides a programming-language-style for expressing verification  \nconditions whose validity implies the correctness of a program under investigation.  \nAs our  \nfocus is on verifying quantitative properties such as bounds on  \nexpected outcomes, expected run-times, or termination  \nprobabilities, off-the-shelf IVLs based on Boolean first-order logic do not  \nsuffice.  \nInstead, a paradigm shift from the standard Boolean to a real-valued domain is required.<\/jats:p>\n          <jats:p>Our IVL features quantitative generalizations of standard  \nverification constructs such as assume- and assert-statements. Verification conditions are generated by a  \nweakest-precondition-style semantics, based on our real-valued logic.  \nWe show that  \nour verification infrastructure supports natural encodings of numerous verification  \ntechniques from the literature. With our SMT-based implementation, we automatically verify a variety of benchmarks. To the best of our knowledge, this establishes the first deductive verification  \ninfrastructure for expectation-based reasoning about probabilistic programs.<\/jats:p>","DOI":"10.1145\/3622870","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"2052-2082","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["A Deductive Verification Infrastructure for Probabilistic Programs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4329-530X","authenticated-orcid":false,"given":"Philipp","family":"Schr\u00f6er","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany \/ University College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"DTU, Kongens Lyngby, Denmark"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428240"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-21963-8_2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_3"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10082-1_6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_28"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_3"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_27"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_7"},{"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\/3571260"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035403"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_22"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58085-9_75"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_30"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268620"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/800061.808758"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/135419.135468"},{"key":"e_1_2_1_51_1","unstructured":"K. Rustan M. Leino. 2008. This Is Boogie 2. \t\t\t\t  K. Rustan M. Leino. 2008. This Is Boogie 2."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"e_1_2_1_54_1","volume-title":"Optimal Discrete Uniform Generation from Coin Flips, and Applications. CoRR, abs\/1304.1916","author":"Lumbroso J\u00e9r\u00e9mie O.","year":"2013","unstructured":"J\u00e9r\u00e9mie O. Lumbroso . 2013. Optimal Discrete Uniform Generation from Coin Flips, and Applications. CoRR, abs\/1304.1916 ( 2013 ), arXiv:1304.1916. arxiv:1304.1916 J\u00e9r\u00e9mie O. Lumbroso. 2013. Optimal Discrete Uniform Generation from Coin Flips, and Applications. CoRR, abs\/1304.1916 (2013), arXiv:1304.1916. arxiv:1304.1916"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158121"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_14"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_18"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_36"},{"key":"e_1_2_1_61_1","unstructured":"Peter M\u00fcller. 2019. Building Deductive Program Verifiers - Lecture Notes. Engineering Secure and Dependable Software Systems. \t\t\t\t  Peter M\u00fcller. 2019. Building Deductive Program Verifiers - Lecture Notes. Engineering Secure and Dependable Software Systems."},{"key":"e_1_2_1_62_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J . Summers . 2016 . Online appendix to Viper : A Verification Infrastructure for Permission-Based Reasoning . http:\/\/viper.ethz.ch\/examples\/vmcai16\/index.html Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Online appendix to Viper: A Verification Infrastructure for Permission-Based Reasoning. http:\/\/viper.ethz.ch\/examples\/vmcai16\/index.html"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v28i1.9060"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935317"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715-6_24"},{"key":"e_1_2_1_71_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_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_4"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8146987"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_8"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563344"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_2_1_77_1","volume-title":"Coupon Collector\u2019s Problem. https:\/\/en.wikipedia.org\/wiki\/Coupon_collector%27s_problem [Online","year":"2023","unstructured":"Wikipedia. 2023. Coupon Collector\u2019s Problem. https:\/\/en.wikipedia.org\/wiki\/Coupon_collector%27s_problem [Online ; accessed 4- September - 2023 ]. Wikipedia. 2023. Coupon Collector\u2019s Problem. https:\/\/en.wikipedia.org\/wiki\/Coupon_collector%27s_problem [Online; accessed 4-September-2023]."},{"key":"e_1_2_1_78_1","volume-title":"Random Walk. https:\/\/en.wikipedia.org\/wiki\/Random_walk#One-dimensional_random_walk [Online","year":"2023","unstructured":"Wikipedia. 2023. Random Walk. https:\/\/en.wikipedia.org\/wiki\/Random_walk#One-dimensional_random_walk [Online ; accessed 4- September - 2023 ]. Wikipedia. 2023. Random Walk. https:\/\/en.wikipedia.org\/wiki\/Random_walk#One-dimensional_random_walk [Online; accessed 4-September-2023]."},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527331"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622870","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622870","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:27Z","timestamp":1750298247000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622870"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":77,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622870"],"URL":"https:\/\/doi.org\/10.1145\/3622870","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}