{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:26:10Z","timestamp":1787592370607,"version":"build-2736575974"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"DFG","award":["GRK 2236 UnRAVeL"],"award-info":[{"award-number":["GRK 2236 UnRAVeL"]}]},{"name":"ERC","award":["Advanced Grant 787914 (FRAPPANT)"],"award-info":[{"award-number":["Advanced Grant 787914 (FRAPPANT)"]}]},{"name":"EU Horizon 2020 Research and Innovation Programme","award":["Marie Sk?odowska-Curie grant No. 101008233 (MISSION)"],"award-info":[{"award-number":["Marie Sk?odowska-Curie grant No. 101008233 (MISSION)"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    We lay out novel foundations for the computer-aided verification of guaranteed bounds on expected outcomes of imperative probabilistic programs featuring (i) general\n                    <jats:italic toggle=\"yes\">loops<\/jats:italic>\n                    , (ii)\n                    <jats:italic toggle=\"yes\">continuous<\/jats:italic>\n                    distributions, and (iii)\n                    <jats:italic toggle=\"yes\">conditioning<\/jats:italic>\n                    . To handle loops we rely on user-provided quantitative\n                    <jats:italic toggle=\"yes\">invariants<\/jats:italic>\n                    , as is well established. However, in the realm of continuous distributions,\n                    <jats:italic toggle=\"yes\">invariant verification<\/jats:italic>\n                    becomes extremely challenging due to the presence of\n                    <jats:italic toggle=\"yes\">integrals<\/jats:italic>\n                    in expectation-based program semantics. Our key idea is to soundly\n                    <jats:italic toggle=\"yes\">under-<\/jats:italic>\n                    or\n                    <jats:italic toggle=\"yes\">over-approximate<\/jats:italic>\n                    these integrals via\n                    <jats:italic toggle=\"yes\">Riemann sums<\/jats:italic>\n                    . We show that this approach enables the SMT-based invariant verification for programs with a fairly general control flow structure. On the theoretical side, we prove\n                    <jats:italic toggle=\"yes\">convergence<\/jats:italic>\n                    of our Riemann approximations, and establish coRE-completeness of the central verification problems. On the practical side, we show that our approach enables to use existing automated verifiers targeting\n                    <jats:italic toggle=\"yes\">discrete<\/jats:italic>\n                    probabilistic programs for the verification of programs involving\n                    <jats:italic toggle=\"yes\">continuous sampling<\/jats:italic>\n                    . Towards this end, we implement our approach in the recent quantitative verification infrastructure Caesar by encoding Riemann sums in its intermediate verification language. We present several promising case studies.\n                  <\/jats:p>","DOI":"10.1145\/3720429","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"421-448","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"},{"name":"University College London, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-3489-9600","authenticated-orcid":false,"given":"Francesca","family":"Randone","sequence":"additional","affiliation":[{"name":"University of Trieste, Trieste, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"Sheshansh Agrawal Krishnendu Chatterjee and Petr Novotn\u00fd. 2017. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. CoRR abs\/1709.04037 (2017). arXiv:1709.04037 http:\/\/arxiv.org\/abs\/1709.04037"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133904"},{"key":"e_1_3_1_5_2","volume-title":"Probability and measure theory","author":"Ash Robert B","year":"2000","unstructured":"Robert B Ash and Catherine A Dol\u00e9ans-Dade. 2000. Probability and measure theory. Academic press."},{"key":"e_1_3_1_6_2","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org."},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632935"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","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 (2) (Lecture Notes in Computer Science Vol. 13994). Springer 410\u2013429. doi:10.1007\/978-3-031-30820-8_25","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3434320"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Kevin Batz Joost-Pieter Katoen Francesca Randone and Tobias Winkler. 2025. Artifact for Paper Foundations for Deductive Verification of Continuous Probabilistic Programs. doi:10.5281\/zenodo.15175355","DOI":"10.5281\/zenodo.15175355"},{"key":"e_1_3_1_11_2","unstructured":"Kevin Batz Joost-Pieter Katoen Francesca Randone and Tobias Winkler. 2025. Foundations for Deductive Verification of Continuous Probabilistic Programs: From Riemann to Lebesgue and Back. CoRR abs\/2502.19388 (2025). https:\/\/arxiv.org\/abs\/2502.19388"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Raven Beutner C.-H. Luke Ong and Fabian Zaiser. 2022. Guaranteed bounds for posterior inference in universal probabilistic programming. In PLDI. ACM 536\u2013551. doi:10.1145\/3519939.3523721","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_3_1_13_2","first-page":"28:1","article-title":"Pyro: Deep Universal Probabilistic Programming","volume":"20","author":"Bingham Eli","year":"2019","unstructured":"Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. 2019. Pyro: Deep Universal Probabilistic Programming. J. Mach. Learn. Res. 20 (2019), 28:1\u201328:6. https:\/\/jmlr.org\/papers\/v20\/18-403.html","journal-title":"J. Mach. Learn. Res"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.7135\/UPO9781614442097"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.18637\/jss.v076.i01"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In CAV (Lecture Notes in Computer Science Vol. 8044). Springer 511\u2013526. doi:10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In SAS (Lecture Notes in Computer Science Vol. 8723). Springer 85\u2013100. doi:10.1007\/978-3-319-10936-7_6","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Hongfei Fu and Amir Kafshdar Goharshady. 2016. Termination Analysis of Probabilistic Programs Through Positivstellensatz\u2019s. In CAV (1) (Lecture Notes in Computer Science Vol. 9779). Springer 3\u201322. doi:10.1007\/978-3-319-41528-4_1","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","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. doi:10.1145\/2837614.2837639","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Amir Kafshdar Goharshady Tobias Meggendorfer and Dorde Zikelic. 2022. Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs. In CAV (1) (Lecture Notes in Computer Science Vol. 13371). Springer 55\u201378. doi:10.1007\/978-3-031-13185-1_4","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656462"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In POPL. ACM 145\u2013160. doi:10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_1_23_2","unstructured":"Michel Coste. 2000. An introduction to semialgebraic geometry."},{"key":"e_1_3_1_24_2","doi-asserted-by":"crossref","unstructured":"Fredrik Dahlqvist Alexandra Silva and Dexter Kozen. 2020. Semantics of probabilistic programming: A gentle introduction. Foundations of Probabilistic Programming (2020) 1\u201342.","DOI":"10.1017\/9781108770750.002"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS (Lecture Notes in Computer Science Vol. 4963). Springer 337\u2013340. doi:10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656412"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Sasa Misailovic and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In CAV (1) (Lecture Notes in Computer Science Vol. 9779). Springer 62\u201383. doi:10.1007\/978-3-319-41528-4_4","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","unstructured":"Timon Gehr Samuel Steffen and Martin T. Vechev. 2020. \u03bbPSI: exact inference for higher-order probabilistic programs. In PLDI. ACM 883\u2013897. doi:10.1145\/3385412.3386006","DOI":"10.1145\/3385412.3386006"},{"key":"e_1_3_1_29_2","unstructured":"Noah D Goodman and Andreas Stuhlm\u00fcller. 2014. The Design and Implementation of Probabilistic Programming Languages. http:\/\/dippl.org. Accessed: 2024-10-15."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","unstructured":"Andrew D. Gordon Thomas A. Henzinger Aditya V. Nori and Sriram K. Rajamani. 2014. Probabilistic programming. In FOSE. ACM 167\u2013181. doi:10.1145\/2593882.2593900","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.PEVA.2013.11.004"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/S11334-021-00433-3"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90004-2"},{"key":"e_1_3_1_35_2","volume-title":"Continuous Univariate Distributions","author":"Johnson N.L.","year":"1995","unstructured":"N.L. Johnson, S. Kotz, and N. Balakrishnan. 1995. Continuous Univariate Distributions, Volume 2. Wiley."},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.18154\/RWTH-2019-01829"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2015. On the Hardness of Almost-Sure Termination. In Mathemat-ical Foundations of Computer Science 2015 - 40th International Symposium MFCS 2015 Milan Italy August 24-28 2015 Proceedings Part I (Lecture Notes in Computer Science Vol. 9234) Giuseppe F. Italiano Giovanni Pighizzini and Donald Sannella (Eds.). Springer 307\u2013318. doi:10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005153"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1016\/0166-218X(91)90086-C"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1983. A Probabilistic PDL. In STOC. ACM 291\u2013297. doi:10.1145\/800061.808758","DOI":"10.1145\/800061.808758"},{"key":"e_1_3_1_41_2","unstructured":"K. Rustan M. Leino. 2008. This Is Boogie 2."},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer. doi:10.1007\/B138392","DOI":"10.1007\/B138392"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-023-00424-Z"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563341"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","unstructured":"Peter M\u00fcller Malte Schwerhoff and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In VMCAI (Lecture Notes in Computer Science Vol. 9583). Springer 41\u201362. doi:10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","unstructured":"Praveen Narayanan Jacques Carette Wren Romano Chung-chieh Shan and Robert Zinkov. 2016. Probabilistic Inference by Program Transformation in Hakaru (System Description). In FLOPS (Lecture Notes in Computer Science Vol. 9613). Springer 62\u201379. doi:10.1007\/978-3-319-29604-3_5","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V28I1.9060"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_3_1_49_2","article-title":"Fixpoint induction and proofs of program properties","volume":"5","author":"Park David","year":"1969","unstructured":"David Park. 1969. Fixpoint induction and proofs of program properties. Machine intelligence 5 (1969).","journal-title":"Machine intelligence"},{"key":"e_1_3_1_50_2","unstructured":"Walter Rudin. 1953. Principles of mathematical analysis."},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","unstructured":"Feras A. Saad Martin C. Rinard and Vikash K. Mansinghka. 2021. SPPL: probabilistic programming with fast exact symbolic inference. In PLDI. ACM 804\u2013819. doi:10.1145\/3453483.3454078","DOI":"10.1145\/3453483.3454078"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","unstructured":"Sriram Sankaranarayanan Aleksandar Chakarov and Sumit Gulwani. 2013. Static analysis for probabilistic programs: inferring whole program properties from finitely many paths. In PLDI. ACM 447\u2013458. doi:10.1145\/2491956.2462179","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622870"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","unstructured":"Marcin Szymczak and Joost-Pieter Katoen. 2019. Weakest Preexpectation Semantics for Bayesian Inference - Condi-tioning Continuous Distributions and Divergence. In SETSS (Lecture Notes in Computer Science Vol. 12154). Springer 44\u2013121. doi:10.1007\/978-3-030-55089-9_3","DOI":"10.1007\/978-3-030-55089-9_3"},{"key":"e_1_3_1_55_2","unstructured":"Jan-Willem van de Meent Brooks Paige Hongseok Yang and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR abs\/1809.10756 (2018). arXiv:1809.10756 http:\/\/arxiv.org\/abs\/1809.10756"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Di Wang Jan Hoffmann and Thomas W. Reps. 2021. Central moment analysis for cost accumulators in probabilistic programs. In PLDI. ACM 559\u2013573. doi:10.1145\/3453483.3454062","DOI":"10.1145\/3453483.3454062"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","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. doi:10.1145\/3453483.3454102","DOI":"10.1145\/3453483.3454102"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","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. doi:10.1145\/3314221.3314581","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_3_1_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656432"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720429","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720429","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:32:25Z","timestamp":1787589145000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720429"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":59,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720429"],"URL":"https:\/\/doi.org\/10.1145\/3720429","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}