{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:10:46Z","timestamp":1775790646639,"version":"3.50.1"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the best of our knowledge,<jats:italic>the first decidability result for the problem of determining whether such a program generates exactly a specified distribution over its outputs<\/jats:italic>(provided the program terminates almost-surely). The class of distributions that can be specified in our formalism consists of standard distributions (geometric, uniform, etc.) and finite convolutions thereof. Our method relies on representing these (possibly infinite-support) distributions as<jats:italic>probability generating functions<\/jats:italic>which admit effective arithmetic operations. We have automated our techniques in a tool called<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {Prodigy}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>P<\/mml:mi><mml:mstyle><mml:mi>R<\/mml:mi><mml:mi>O<\/mml:mi><mml:mi>D<\/mml:mi><mml:mi>I<\/mml:mi><mml:mi>G<\/mml:mi><mml:mi>Y<\/mml:mi><\/mml:mstyle><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, which supports automatic invariance checking, compositional reasoning of nested loops, and efficient queries to the output distribution, as demonstrated by experiments.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_5","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"79-101","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Does a\u00a0Program Yield the\u00a0Right Distribution?"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9663-7441","authenticated-orcid":false,"given":"Mingshuai","family":"Chen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3812-0572","authenticated-orcid":false,"given":"Lutz","family":"Klinkenberg","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Arvo, J., Kirk, D.B.: Particle transport and image synthesis. In: SIGGRAPH, pp. 63\u201366. ACM (1990)","DOI":"10.1145\/97880.97886"},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/0196-6774(90)90021-6","volume":"11","author":"J Aspnes","year":"1990","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. J. Algorithms 11(3), 441\u2013461 (1990)","journal-title":"J. Algorithms"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101. ACM (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Jacomme, C., Kremer, S.: Universal equivalence and majority of probabilistic programs over finite fields. In: LICS, pp. 155\u2013166. ACM (2020)","DOI":"10.1145\/3373718.3394746"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Katoen, J., Silva, A. (eds.): Foundations of Probabilistic Programming. Cambridge University Press, Cambridge (2020)","DOI":"10.1017\/9781108770750"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., B\u00e9guelin, S.Z.: Probabilistic relational reasoning for differential privacy. ACM Trans. Program. Lang. Syst. 35(3), 9:1\u20139:49 (2013)","DOI":"10.1145\/2492061"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-030-64276-1_12","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2020","author":"E Bartocci","year":"2020","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovi\u010d, M.: Analysis of Bayesian networks via prob-solvable loops. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) ICTAC 2020. LNCS, vol. 12545, pp. 221\u2013241. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64276-1_12"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-030-45190-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2020","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovi\u010d, M.: Mora - automatic generation of moment-based invariants. In: TACAS 2020. LNCS, vol. 12078, pp. 492\u2013498. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_28"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1007\/978-3-030-81688-9_25","volume-title":"Computer Aided Verification","author":"K Batz","year":"2021","unstructured":"Batz, K., Chen, M., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: Latticed k-induction with an application to probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 524\u2013549. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25"},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jsco.2001.0494","volume":"33","author":"C Bauer","year":"2002","unstructured":"Bauer, C., Frink, A., Kreckel, R.: Introduction to the GiNaC framework for symbolic computation within the C++ programming language. J. Symb. Comput. 33(1), 1\u201312 (2002)","journal-title":"J. Symb. Comput."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Bhat, S., Agarwal, A., Vuduc, R.W., Gray, A.G.: A type theory for probability density functions. In: POPL, pp. 545\u2013556. ACM (2012)","DOI":"10.1145\/2103621.2103721"},{"key":"5_CR12","unstructured":"Bhat, S., Borgstr\u00f6m, J., Gordon, A.D., Russo, C.V.: Deriving probability density functions from probabilistic functional programs. Log. Methods Comput. Sci. 13(2) (2017)"},{"issue":"8","key":"5_CR13","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/2958738","volume":"59","author":"M Carbin","year":"2016","unstructured":"Carbin, M., Misailovic, S., Rinard, M.C.: Verifying quantitative reliability for programs that execute on unreliable hardware. Commun. ACM 59(8), 83\u201391 (2016)","journal-title":"Commun. ACM"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-319-28228-2_9","volume-title":"Practical Aspects of Declarative Languages","author":"J Carette","year":"2016","unstructured":"Carette, J., Shan, C.-C.: Simplifying probabilistic programs using computer algebra. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 135\u2013152. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-28228-2_9"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P.: Termination analysis of probabilistic programs with martingales, pp. 221\u2013258. In: Barthe et al. [5] (2020)","DOI":"10.1017\/9781108770750.008"},{"key":"5_CR18","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. CoRR abs\/2205.01449 (2022)","DOI":"10.1007\/978-3-031-13185-1_5"},{"issue":"8","key":"5_CR19","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)","journal-title":"Commun. ACM"},{"key":"5_CR20","unstructured":"Evans, O., Stuhlm\u00fcller, A., Salvatier, J., Filan, D.: Modeling agents with probabilistic programs. http:\/\/agentmodels.org (2017). Accessed 17 Jan 2022"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Flajolet, P., Pelletier, M., Soria, M.: On Buffon machines and numbers. In: SODA, pp. 172\u2013183. SIAM (2011)","DOI":"10.1137\/1.9781611973082.15"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics. Cambridge University Press, Cambridge (2009)","DOI":"10.1017\/CBO9780511801655"},{"key":"5_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.ic.2014.04.003","volume":"237","author":"V Forejt","year":"2014","unstructured":"Forejt, V., Jancar, P., Kiefer, S., Worrell, J.: Language equivalence of probabilistic pushdown automata. Inf. Comput. 237, 1\u201311 (2014)","journal-title":"Inf. Comput."},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-41528-4_4","volume-title":"Computer Aided Verification","author":"T Gehr","year":"2016","unstructured":"Gehr, T., Misailovic, S., Vechev, M.: PSI: exact symbolic inference for probabilistic programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 62\u201383. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Gehr, T., Steffen, S., Vechev, M.T.: $$\\lambda $$PSI: exact inference for higher-order probabilistic programs. In: PLDI, pp. 883\u2013897. ACM (2020)","DOI":"10.1145\/3385412.3386006"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic programming. In: FOSE, pp. 167\u2013181. ACM (2014)","DOI":"10.1145\/2593882.2593900"},{"key":"5_CR27","unstructured":"Hammersley, J.: Monte Carlo Methods. Springer Science & Business Media (2013)"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Hark, M., Kaminski, B.L., Giesl, J., Katoen, J.: Aiming low is harder: induction for lower bounds in probabilistic program verification. Proc. ACM Program. Lang. 4(POPL), 37:1\u201337:28 (2020)","DOI":"10.1145\/3371105"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Heninger, N.: RSA, DH and DSA in the wild. In: Bos, J., Stam, M. (eds.) Computational Cryptography: Algorithmic Aspects of Cryptology, pp. 140\u2013181. Cambridge University Press, Cambridge (2021)","DOI":"10.1017\/9781108854207.008"},{"key":"5_CR30","unstructured":"Hicks, M.: What is probabilistic programming? In: The Programming Languages Enthusiast (2014). http:\/\/www.pl-enthusiast.net\/2014\/09\/08. Accessed 09 Dec 2021"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Holtzen, S., den Broeck, G.V., Millstein, T.D.: Scaling exact inference for discrete probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 140:1\u2013140:31 (2020)","DOI":"10.1145\/3428208"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-030-88885-5_16","volume-title":"Automated Technology for Verification and Analysis","author":"Z Huang","year":"2021","unstructured":"Huang, Z., Dutta, S., Misailovic, S.: AQUA: automated quantized inference for probabilistic programs. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 229\u2013246. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_16"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Zanasi, F.: The logical essentials of Bayesian reasoning, pp. 295\u2013331. In: Barthe et al. [5] (2020)","DOI":"10.1017\/9781108770750.010"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-319-46520-3_5","volume-title":"Automated Technology for Verification and Analysis","author":"N Jansen","year":"2016","unstructured":"Jansen, N., Dehnert, C., Kaminski, B.L., Katoen, J.-P., Westhofen, L.: Bounded model checking for probabilistic programs. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 68\u201385. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_5"},{"key":"5_CR35","unstructured":"Johnson, N., Kotz, S., Kemp, A.: Univariate Discrete Distributions. Wiley, Hoboken (1993)"},{"key":"5_CR36","unstructured":"Jones, C.: Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, UK (1990)"},{"key":"5_CR37","doi-asserted-by":"crossref","unstructured":"Kajiya, J.T.: The rendering equation. In: SIGGRAPH, pp. 143\u2013150. ACM (1986)","DOI":"10.1145\/15886.15902"},{"key":"5_CR38","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019)"},{"issue":"3","key":"5_CR39","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/s00236-018-0321-1","volume":"56","author":"BL Kaminski","year":"2018","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Informatica 56(3), 255\u2013285 (2018). https:\/\/doi.org\/10.1007\/s00236-018-0321-1","journal-title":"Acta Informatica"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1\u201330:68 (2018)","DOI":"10.1145\/3208102"},{"key":"5_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/978-3-642-22110-1_42","volume-title":"Computer Aided Verification","author":"S Kiefer","year":"2011","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: Language\u00a0equivalence\u00a0for probabilistic\u00a0automata. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 526\u2013540. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_42"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-68446-4_12","volume-title":"Logic-Based Program Synthesis and Transformation","author":"L Klinkenberg","year":"2021","unstructured":"Klinkenberg, L., Batz, K., Kaminski, B.L., Katoen, J.-P., Moerman, J., Winkler, T.: Generating functions for probabilistic programs. In: Fern\u00e1ndez, M. (ed.) LOPSTR 2020. LNCS, vol. 12561, pp. 231\u2013248. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_12"},{"issue":"3","key":"5_CR43","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"5_CR44","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985)","journal-title":"J. Comput. Syst. Sci."},{"key":"5_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-78800-3_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Legay","year":"2008","unstructured":"Legay, A., Murawski, A.S., Ouaknine, J., Worrell, J.: on automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 173\u2013187. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_13"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof For Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"5_CR47","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. PACMPL 2(POPL), 33:1\u201333:28 (2018)","DOI":"10.1145\/3158121"},{"key":"5_CR48","unstructured":"van de Meent, J., Paige, B., Yang, H., Wood, F.: An introduction to probabilistic programming. CoRR abs\/1809.10756 (2018)"},{"key":"5_CR49","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. PeerJ Comput. Sci. 3, e103 (2017)","journal-title":"PeerJ Comput. Sci."},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1007\/978-3-030-90870-6_36","volume-title":"Formal Methods","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: The probabilistic termination tool amber. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 667\u2013675. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_36"},{"key":"5_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11539452_15","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"AS Murawski","year":"2005","unstructured":"Murawski, A.S., Ouaknine, J.: On probabilistic program equivalence and refinement. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 156\u2013170. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11539452_15"},{"key":"5_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-29604-3_5","volume-title":"Functional and Logic Programming","author":"P Narayanan","year":"2016","unstructured":"Narayanan, P., Carette, J., Romano, W., Shan, C., Zinkov, R.: Probabilistic inference by program transformation in Hakaru (system description). In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 62\u201379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_5"},{"issue":"1","key":"5_CR53","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/151254.151256","volume":"25","author":"M Schneider","year":"1993","unstructured":"Schneider, M.: Self-stabilization. ACM Comput. Surv. 25(1), 45\u201367 (1993)","journal-title":"ACM Comput. Surv."},{"key":"5_CR54","doi-asserted-by":"crossref","unstructured":"Shamsi, S.M., Farina, G.P., Gaboardi, M., Napp, N.: Probabilistic programming languages for modeling autonomous systems. In: MFI, pp. 32\u201339. IEEE (2020)","DOI":"10.1109\/MFI49285.2020.9235230"},{"key":"5_CR55","doi-asserted-by":"crossref","unstructured":"Tijms, H.C.: A First Course in Stochastic Models. Wiley, Hoboken (2003)","DOI":"10.1002\/047001363X"},{"issue":"2","key":"5_CR56","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1137\/0221017","volume":"21","author":"W Tzeng","year":"1992","unstructured":"Tzeng, W.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM J. Comput. 21(2), 216\u2013227 (1992)","journal-title":"SIAM J. Comput."},{"issue":"1","key":"5_CR57","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/j.nima.2005.11.155","volume":"559","author":"J Vollinga","year":"2006","unstructured":"Vollinga, J.: GiNaC-symbolic Computation with C++. Nucl. Instrum. Methods Phys. Res. 559(1), 282\u2013284 (2006)","journal-title":"Nucl. Instrum. Methods Phys. Res."},{"key":"5_CR58","doi-asserted-by":"crossref","unstructured":"Wang, D., Hoffmann, J., Reps, T.W.: Central moment analysis for cost accumulators in probabilistic programs. In: PLDI, pp. 559\u2013573. ACM (2021)","DOI":"10.1145\/3410293"},{"key":"5_CR59","doi-asserted-by":"crossref","unstructured":"Wang, J., Sun, Y., Fu, H., Chatterjee, K., Goharshady, A.K.: Quantitative analysis of assertion violations in probabilistic programs. In: PLDI, pp. 1171\u20131186. ACM (2021)","DOI":"10.1145\/3410310"},{"key":"5_CR60","unstructured":"Wilf, H.S.: Generating Functionology. CRC Press, Boca Raton (2005)"},{"key":"5_CR61","doi-asserted-by":"crossref","unstructured":"Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. 33(6), 19:1\u201319:49 (2011)","DOI":"10.1145\/2049706.2049708"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,30]],"date-time":"2024-09-30T22:06:09Z","timestamp":1727733969000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_5"}},"subtitle":["Verifying Probabilistic Programs via Generating Functions"],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}