@article{KlinkenbergBlumenthalChenHaaseKatoen:OOPSLA:2024,
    author = {Klinkenberg, Lutz and Blumenthal, Christian and Chen, Mingshuai and Haase, Darion and Katoen, Joost-Pieter},
    title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions},
    year = {2024},
    issue_date = {April 2024},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    volume = {8},
    number = {OOPSLA1},
    url = {https://doi.org/10.1145/3649844},
    doi = {10.1145/3649844},
    abstract = {We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (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.},
    journal = {Proc. ACM Program. Lang.},
    month = {apr},
    articleno = {127},
    numpages = {31},
    keywords = {Bayesian inference, conditioning, denotational semantics, generating functions, non-termination, probabilistic programs, quantitative verification},
    date-added = {2024-9-2 7:26:22 +0100}
}

@article{KlinkenbergBlumenthalChenHaaseKatoen:OOPSLA:2024, author = {Klinkenberg, Lutz and Blumenthal, Christian and Chen, Mingshuai and Haase, Darion and Katoen, Joost-Pieter}, title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions}, year = {2024}, issue_date = {April 2024}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {8}, number = {OOPSLA1}, url = {https://doi.org/10.1145/3649844}, doi = {10.1145/3649844}, abstract = {We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (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.}, journal = {Proc. ACM Program. Lang.}, month = {apr}, articleno = {127}, numpages = {31}, keywords = {Bayesian inference, conditioning, denotational semantics, generating functions, non-termination, probabilistic programs, quantitative verification}, date-added = {2024-9-2 7:26:22 +0100} }