{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:01Z","timestamp":1784675041145,"version":"3.55.0"},"reference-count":94,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"European Research Council","award":["AdG Grant 787914"],"award-info":[{"award-number":["AdG Grant 787914"]}]},{"name":"Deutsche Forschungsgemeinschaft","award":["RTG 2236 UnRAVeL"],"award-info":[{"award-number":["RTG 2236 UnRAVeL"]}]},{"name":"Zhejiang Provincial Natural Science Foundation","award":["Major Program LD24F020013"],"award-info":[{"award-number":["Major Program LD24F020013"]}]},{"name":"ZJU Education Foundation","award":["Qizhen Talent program"],"award-info":[{"award-number":["Qizhen Talent program"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>\n            We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly\n            <jats:italic>unbounded loops<\/jats:italic>\n            . Our method is built on a denotational semantics represented by\n            <jats:italic>probability generating functions<\/jats:italic>\n            , which resolves semantic intricacies induced by intertwining discrete probabilistic loops with\n            <jats:italic>conditioning<\/jats:italic>\n            (for encoding posterior observations). We implement our method in a tool called Prodigy; it augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs. Experimental results show that Prodigy can handle various infinite-state loopy programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks.\n          <\/jats:p>","DOI":"10.1145\/3649844","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"923-953","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3812-0572","authenticated-orcid":false,"given":"Lutz","family":"Klinkenberg","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6427-0229","authenticated-orcid":false,"given":"Christian","family":"Blumenthal","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"additional","affiliation":[{"name":"Zhejiang University, Hangzhou, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5664-6773","authenticated-orcid":false,"given":"Darion","family":"Haase","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Aachen, Germany"}],"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"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3321699"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/S002360050117"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_3"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-64276-1_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_28"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_27"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0494"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103721"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(2:16)2017"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_6"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2958738"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31514-6_7"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.008"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and Dorde Zikelic. 2017. Stochastic Invariants for Probabilistic Termination. In POPL. ACM 145\u2013160. https:\/\/doi.org\/10.1145\/3009837.3009873 10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2205.01449"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_44"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586050"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(90)90060-D"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750.002"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44804-7_3"},{"key":"e_1_2_1_32_1","volume-title":"Concentration of Measure for the Analysis of Randomized Algorithms","author":"Dubhashi Devdatt P","unstructured":"Devdatt P Dubhashi and Alessandro Panconesi. 2009. Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586051"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973082.15"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Philippe Flajolet and Robert Sedgewick. 2009. Analytic Combinatorics. Cambridge University Press. https:\/\/doi.org\/10.1017\/CBO9780511801655 10.1017\/CBO9780511801655","DOI":"10.1017\/CBO9780511801655"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10994-021-06120-5"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386006"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_41_1","volume-title":"Extending probabilistic programming systems and applying them to real-world simulators. Ph. D. Dissertation","author":"Gram-Hansen Bradley","unstructured":"Bradley Gram-Hansen. 2021. Extending probabilistic programming systems and applying them to real-world simulators. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371105"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88885-5_16"},{"key":"e_1_2_1_47_1","volume-title":"IL, 2023","author":"Research Wolfram","year":"2023","unstructured":"Wolfram Research, Inc.. 2023. Mathematica, Version 13.3. https:\/\/www.wolfram.com\/mathematica Champaign, IL, 2023"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434339"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_5"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1002\/0471715816"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.18154\/RWTH-2019-01829"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Joost-Pieter Katoen. 2016. The Probabilistic Model Checking Landscape. In LICS. ACM 31\u201345. https:\/\/doi.org\/10.1145\/2933575.2934574 10.1145\/2933575.2934574","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_12"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2307.07314"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Lutz Klinkenberg Christian Blumenthal Mingshuai Chen Darion Haase and Joost-Pieter Katoen. 2024. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions \u2013 Artifact. https:\/\/doi.org\/10.5281\/zenodo.10782412 10.5281\/zenodo.10782412","DOI":"10.5281\/zenodo.10782412"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2302.00513"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_61_1","volume-title":"The computational complexity of probabilistic networks. Ph. D. Dissertation","author":"Petrus Kwisthout Johan Henri","unstructured":"Johan Henri Petrus Kwisthout. 2009. The computational complexity of probabilistic networks. Ph. D. Dissertation. Utrecht University."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1613\/JAIR.505"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/B138392"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1949.10483310"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103"},{"key":"e_1_2_1_66_1","volume-title":"BLOG: Probabilistic Models with Unknown Objects. In IJCAI. 1352\u20131359.","author":"Milch Brian","year":"2005","unstructured":"Brian Milch, Bhaskara Marthi, Stuart Russell, David A. Sontag, Daniel L. Ong, and Andrey Kolobov. 2005. BLOG: Probabilistic Models with Unknown Objects. In IJCAI. 1352\u20131359."},{"key":"e_1_2_1_67_1","unstructured":"Tom Minka John M. Winn John P. Guiver Yordan Zaykov Dany Fabian and John Bronskill. 2018. Infer.NET 0.3. http:\/\/dotnet.github.io\/infer Microsoft Research Cambridge"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813603"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563341"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V28I1.9060"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_27"},{"key":"e_1_2_1_74_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)."},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Marko Petkovsek Herbert S Wilf and Doron Zeilberger. 1996. A = B. CRC Press. isbn:9781439864500","DOI":"10.1201\/9781439864500"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_92"},{"key":"e_1_2_1_79_1","volume-title":"ICML (PMLR","volume":"4630","author":"Sheldon Daniel","year":"2018","unstructured":"Daniel Sheldon, Kevin Winner, and Debora Sujono. 2018. Learning in Integer Latent Variable Models with Nested Automatic Differentiation. In ICML (PMLR, Vol. 80). PMLR, 4622\u20134630."},{"key":"e_1_2_1_80_1","first-page":"50","article-title":"BUGS: Bayesian Inference Using Gibbs Sampling","volume":"0","author":"Spiegelhalter David J.","year":"1995","unstructured":"David J. Spiegelhalter, Andrew Thomas, Nicola G. Best, and Walter R. Gilks. 1995. BUGS: Bayesian Inference Using Gibbs Sampling, Version 0.50.","journal-title":"Version"},{"key":"e_1_2_1_81_1","first-page":"31","article-title":"Stan Modeling Language Users Guide and Reference Manual","volume":"2","author":"Team Stan Development","year":"2022","unstructured":"Stan Development Team. 2022. Stan Modeling Language Users Guide and Reference Manual, Version 2.31.","journal-title":"Version"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470552"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1206.3555"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1809.10756"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.nima.2005.11.155"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454062"},{"key":"e_1_2_1_88_1","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. https:\/\/doi.org\/10.1145\/3453483.3454102 10.1145\/3453483.3454102","DOI":"10.1145\/3453483.3454102"},{"key":"e_1_2_1_89_1","unstructured":"Herbert S Wilf. 2005. Generatingfunctionology. CRC press."},{"key":"e_1_2_1_90_1","unstructured":"Kevin Winner and Daniel Sheldon. 2016. Probabilistic Inference with Generating Functions for Poisson Latent Variable Models. In NIPS. 2640\u20132648."},{"key":"e_1_2_1_91_1","volume-title":"ICML (PMLR","volume":"3770","author":"Winner Kevin","year":"2017","unstructured":"Kevin Winner, Debora Sujono, and Daniel Sheldon. 2017. Exact Inference for Integer Latent-Variable Models. In ICML (PMLR, Vol. 70). PMLR, 3761\u20133770."},{"key":"e_1_2_1_92_1","first-page":"1024","article-title":"A New Approach to Probabilistic Programming Inference","author":"Wood Frank D.","year":"2014","unstructured":"Frank D. Wood, Jan-Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In AISTATS. 33, JMLR.org, 1024\u20131032.","journal-title":"AISTATS. 33, JMLR.org"},{"key":"e_1_2_1_93_1","unstructured":"Fabian Zaiser Andrzej S. Murawski and C.-H. Luke Ong. 2023. Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach. In NeurIPS. To appear"},{"key":"e_1_2_1_94_1","unstructured":"Fabian Zaiser and C.-H. Luke Ong. 2023. Exact Inference for Discrete Probabilistic Programs via Generating Functions. https:\/\/popl23.sigplan.org\/details\/lafi-2023-papers\/10\/Exact-Inference-for-Discrete-Probabilistic-Programs-via-Generating-Functions"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649844","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649844","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649844"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":94,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649844"],"URL":"https:\/\/doi.org\/10.1145\/3649844","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}