{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T19:07:06Z","timestamp":1783019226945,"version":"3.54.6"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032262035","type":"print"},{"value":"9783032262042","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"vor","delay-in-days":137,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    This paper presents a Hoare-like verification framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso\u2019s\n                    <jats:italic>Fast Dice Roller<\/jats:italic>\n                    and Saad et al.\u2019s\n                    <jats:italic>Fast Loaded Dice Roller<\/jats:italic>\n                    . These algorithms have previously resisted formal verification due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-26204-2_14","type":"book-chapter","created":{"date-parts":[[2026,5,17]],"date-time":"2026-05-17T15:51:15Z","timestamp":1779033075000},"page":"259-278","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying Sampling Algorithms via\u00a0Distributional Invariants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-7221-2554","authenticated-orcid":false,"given":"Daniel","family":"Zilken","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,18]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Aghamov, R., et al.: Model checking Markov Chains as distribution transformers. In: Principles of Verification (2). Lecture Notes in Computer Science, vol. 15261, pp. 293\u2013313. Springer (2024)","DOI":"10.1007\/978-3-031-75775-4_13"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Akshay, S., Chatterjee, K., Meggendorfer, T., Zikelic, D.: MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives. In: Computer Aided Verification, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 86\u2013112. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_5,","DOI":"10.1007\/978-3-031-37709-9_5"},{"key":"14_CR3","unstructured":"Akshay, S., Chatterjee, K., Meggendorfer, T., Zikelic, D.: Certified policy verification and synthesis for MDPS under distributional reach-avoidance properties. In: IJCAI, pp. 3\u201312. ijcai.org (2024)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Akshay, S., Genest, B., Vyas, N.: Distribution-based objectives for Markov Decision Processes. In: LICS, pp. 36\u201345. ACM (2018)","DOI":"10.1145\/3209108.3209185"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Bagnall, A., Stewart, G., Banerjee, A.: Formally verified samplers from probabilistic programs with loops and conditioning. Proc. ACM Program. Lang. 7(PLDI), 1\u201324 (2023). https:\/\/doi.org\/10.1145\/3591220,","DOI":"10.1145\/3591220"},{"key":"14_CR6","unstructured":"Baier, C., Katoen, J.: Principles of model checking. MIT Press (2008)"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Espitau, T., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: An assertion-based program logic for probabilistic programs. In: Programming Languages and Systems. Lecture Notes in Computer Science, vol. 10801, pp. 117\u2013144. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5,","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Batz, K., Katoen, J., Winkler, T., Zilken, D.: Verifying sampling algorithms via distributional invariants. CoRR abs\/2509.06410 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2509.06410,","DOI":"10.48550\/ARXIV.2509.06410"},{"key":"14_CR9","doi-asserted-by":"publisher","unstructured":"Beutner, R., Ong, C.L., Zaiser, F.: Guaranteed bounds for posterior inference in universal probabilistic programming. In: PLDI, pp. 536\u2013551 (2022). ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523721,","DOI":"10.1145\/3519939.3523721"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Meel, K.S.: On testing of uniform samplers, pp. 7777\u20137784. AAAI Press (2019). https:\/\/doi.org\/10.1609\/AAAI.V33I01.33017777","DOI":"10.1609\/AAAI.V33I01.33017777"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Goharshady, E.K., Novotn\u00fd, P., Zikelic, D.: Equivalence and similarity refutation for probabilistic programs. Proc. ACM Program. Lang. 8(PLDI), 2098\u20132122 (2024). https:\/\/doi.org\/10.1145\/3656462,","DOI":"10.1145\/3656462"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Chen, M., Katoen, J., Klinkenberg, L., Winkler, T.: Does a program yield the right distribution? - verifying probabilistic programs via generating functions. In: CAV (1). Lecture Notes in Computer Science, vol. 13371, pp. 79\u2013101. Springer (2022)","DOI":"10.1007\/978-3-031-13185-1_5"},{"issue":"48","key":"14_CR13","doi-asserted-by":"publisher","first-page":"30055","DOI":"10.1073\/pnas.1912789117","volume":"117","author":"K Cranmer","year":"2020","unstructured":"Cranmer, K., Brehmer, J., Louppe, G.: The frontier of simulation-based inference. Proc. Natl. Acad. Sci. 117(48), 30055\u201330062 (2020). https:\/\/doi.org\/10.1073\/pnas.1912789117","journal-title":"Proc. Natl. Acad. Sci."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Dahlqvist, F., Silva, A., Smith, W.: Deterministic stream-sampling for probabilistic programming: semantics and verification. In: LICS, pp. 1\u201313. IEEE (2023)","DOI":"10.1109\/LICS56636.2023.10175773"},{"issue":"8","key":"14_CR15","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975). https:\/\/doi.org\/10.1145\/360933.360975","journal-title":"Commun. ACM"},{"key":"14_CR16","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Gehr, T., Misailovic, S., Vechev, M.T.: PSI: exact symbolic inference for probabilistic programs. In: CAV (1). Lecture Notes in Computer Science, vol.\u00a09779, pp. 62\u201383. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"14_CR18","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press (2016)"},{"key":"14_CR19","unstructured":"Haase, D., et al.: Generating functions meet occupation measures: Invariant synthesis for probabilistic loops (extended version) (2026). https:\/\/arxiv.org\/abs\/2601.13991, to appear at ESOP 2026"},{"issue":"3","key":"14_CR20","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1142\/S012905410200114X","volume":"13","author":"J den Hartog","year":"2002","unstructured":"den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a hoare like logic. Int. J. Found. Comput. Sci. 13(3), 315\u2013340 (2002). https:\/\/doi.org\/10.1142\/S012905410200114X","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"4","key":"14_CR21","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR22","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.jcss.2021.02.006","volume":"119","author":"S Junges","year":"2021","unstructured":"Junges, S., Katoen, J., P\u00e9rez, G.A., Winkler, T.: The complexity of reachability in parametric Markov decision processes. J. Comput. Syst. Sci. 119, 183\u2013210 (2021)","journal-title":"J. Comput. Syst. Sci."},{"key":"14_CR23","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019). http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Klinkenberg, L., Batz, K., Kaminski, B.L., Katoen, J., Moerman, J., Winkler, T.: Generating functions for probabilistic programs. In: Logic-Based Program Synthesis and Transformation. Lecture Notes in Computer Science, vol. 12561, pp. 231\u2013248. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_12,","DOI":"10.1007\/978-3-030-68446-4_12"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of probabilistic programs. In: 20th Annual Symposium on Foundations of Computer Science, pp. 101\u2013114. IEEE Computer Society (1979). https:\/\/doi.org\/10.1109\/SFCS.1979.38,","DOI":"10.1109\/SFCS.1979.38"},{"key":"14_CR26","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A probabilistic PDL. In: Proceedings of the 15th Annual ACM Symposium on Theory of Computing, pp. 291\u2013297. ACM (1983). https:\/\/doi.org\/10.1145\/800061.808758","DOI":"10.1145\/800061.808758"},{"key":"14_CR27","unstructured":"Lumbroso, J.O.: Optimal discrete uniform generation from coin flips, and applications. CoRR arXiv:abs\/1304.1916 (2013)"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang. 9(POPL), 1871\u20131902 (2025)","DOI":"10.1145\/3704899"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science, Springer (2005).https:\/\/doi.org\/10.1007\/B138392","DOI":"10.1007\/B138392"},{"key":"14_CR30","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. 2(POPL) (Dec 2017). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"issue":"3","key":"14_CR31","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/S10817-025-09736-7","volume":"69","author":"H Mertens","year":"2025","unstructured":"Mertens, H., Katoen, J., Quatmann, T., Winkler, T.: Computing expected visiting times and stationary distributions in Markov chains: fast and accurate. J. Autom. Reason. 69(3), 23 (2025). https:\/\/doi.org\/10.1007\/S10817-025-09736-7","journal-title":"J. Autom. Reason."},{"issue":"6","key":"14_CR32","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"WW Pugh","year":"1990","unstructured":"Pugh, W.W.: Skip lists: a probabilistic alternative to balanced trees. Commun. ACM 33(6), 668\u2013676 (1990). https:\/\/doi.org\/10.1145\/78973.78977","journal-title":"Commun. ACM"},{"key":"14_CR33","unstructured":"Saad, F., Freer, C.E., Rinard, M.C., Mansinghka, V.: The fast loaded dice roller: a near-optimal exact sampler for discrete probability distributions. In: The 23rd International Conference on Artificial Intelligence and Statistics, AISTATS 2020. Proceedings of Machine Learning Research, vol.\u00a0108, pp. 1036\u20131046. PMLR (2020). http:\/\/proceedings.mlr.press\/v108\/saad20a.html"},{"key":"14_CR34","doi-asserted-by":"publisher","unstructured":"Sarkar, U., Chakraborty, S., Meel, K.S.: Assessing the quality of binomial samplers: A statistical distance framework. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II. Lecture Notes in Computer Science, vol. 15932, pp. 231\u2013253. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_11,","DOI":"10.1007\/978-3-031-98679-6_11"},{"issue":"36\u201338","key":"14_CR35","first-page":"5","volume":"12","author":"J Von Neumann","year":"1951","unstructured":"Von Neumann, J.: Various techniques used in connection with random digits. Appl. Math Ser 12(36\u201338), 5 (1951)","journal-title":"Appl. Math Ser"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Wang, P., Yang, T., Fu, H., Li, G., Ong, C.H.L.: Static posterior inference of bayesian probabilistic programming via polynomial solving. Proc. ACM Programm. Lang. 8(PLDI), 1361\u20131386 (2024). https:\/\/doi.org\/10.1145\/3656432","DOI":"10.1145\/3656432"},{"key":"14_CR37","doi-asserted-by":"publisher","unstructured":"Zilberstein, N.: Outcome logic: A unified approach to the metatheory of program logics with branching effects. ACM Trans. Program. Lang. Syst. 47(3) (Sept 2025). https:\/\/doi.org\/10.1145\/3743131,","DOI":"10.1145\/3743131"},{"key":"14_CR38","doi-asserted-by":"publisher","unstructured":"Zilberstein, N., Kozen, D., Silva, A., Tassarotti, J.: A demonic outcome logic for randomized nondeterminism. Proc. ACM Programm. Lang. 9(POPL), 539\u2013568 (Jan 2025). https:\/\/doi.org\/10.1145\/3704855","DOI":"10.1145\/3704855"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-26204-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T17:56:21Z","timestamp":1783014981000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-26204-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032262035","9783032262042"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-26204-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"18 May 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tokyo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/fm-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}