{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:49Z","timestamp":1779087709215,"version":"3.51.4"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030684457","type":"print"},{"value":"9783030684464","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-68446-4_12","type":"book-chapter","created":{"date-parts":[[2021,2,12]],"date-time":"2021-02-12T19:06:39Z","timestamp":1613156799000},"page":"231-248","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Generating Functions for Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3812-0572","authenticated-orcid":false,"given":"Lutz","family":"Klinkenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9819-8374","authenticated-orcid":false,"given":"Joshua","family":"Moerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,2,13]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Hsu, J., Strub, P.: Coupling proofs are probabilistic product programs. In: POPL, pp. 161\u2013174. ACM (2017)","DOI":"10.1145\/3093333.3009896"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-030-31784-3_15","volume-title":"Automated Technology for Verification and Analysis","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovi\u010d, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 255\u2013276. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Noll, T.: Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. In: PACMPL 3 (POPL), pp. 34:1\u201334:29 (2019)","DOI":"10.1145\/3290347"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-662-47666-6_7","volume-title":"Automata, Languages, and Programming","author":"M Boreale","year":"2015","unstructured":"Boreale, M.: Analysis of probabilistic systems via generating functions and Pad\u00e9 approximation. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 82\u201394. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_7"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-662-49674-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bouissou","year":"2016","unstructured":"Bouissou, O., Goubault, E., Putot, S., Chakarov, A., Sankaranarayanan, S.: Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 225\u2013243. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_13"},{"key":"12_CR6","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":"12_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. 40(2), 7:1\u20137:45 (2018)","DOI":"10.1145\/3174800"},{"key":"12_CR8","unstructured":"Cho, K., Jacobs, B.: The EfProb library for probabilistic calculations. In: CALCO. LIPIcs, vol. 72, pp. 25:1\u201325:8. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-28869-2_9","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2012","unstructured":"Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 169\u2013193. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_9"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/978-3-319-03542-0_18","volume-title":"Programming Languages and Systems","author":"A Di Pierro","year":"2013","unstructured":"Di Pierro, A., Wiklicky, H.: Semantics of probabilistic programs: a weak limit approach. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 241\u2013256. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_18"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-030-29436-6_16","volume-title":"Automated Deduction \u2013 CADE 27","author":"J Giesl","year":"2019","unstructured":"Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 269\u2013286. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_16"},{"key":"12_CR12","volume-title":"Concrete Mathematics: A Foundation for Computer Science","author":"R Graham","year":"1994","unstructured":"Graham, R., Knuth, D., Patashnik, O.: Concrete Mathematics: A Foundation for Computer Science. Addison-Wesley, Boston (1994)"},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/j.peva.2013.11.004","volume":"73","author":"F Gretz","year":"2014","unstructured":"Gretz, F., Katoen, J., McIver, A.: Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73, 110\u2013132 (2014)","journal-title":"Perform. Eval."},{"key":"12_CR14","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"},{"issue":"3","key":"12_CR15","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)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-45685-6_16","volume-title":"Theorem Proving in Higher Order Logics","author":"J Hurd","year":"2002","unstructured":"Hurd, J.: A formal approach to probabilistic termination. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230\u2013245. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45685-6_16"},{"key":"12_CR17","doi-asserted-by":"publisher","first-page":"102308","DOI":"10.1016\/j.jmp.2019.102308","volume":"95","author":"T Icard","year":"2020","unstructured":"Icard, T.: Calibrating generative models: the probabilistic Chomsky-Sch\u00fctzenberger hierarchy. J. Math. Psychol. 95, 102308 (2020). https:\/\/www.sciencedirect.com\/journal\/journal-of-mathematical-psychology\/vol\/95\/suppl\/C","journal-title":"J. Math. Psychol."},{"key":"12_CR18","unstructured":"Inc., W.R.: Mathematica, Version 12.0, champaign, IL (2019). https:\/\/www.wolfram.com\/mathematica"},{"key":"12_CR19","volume-title":"Univariate Discrete Distributions","author":"N Johnson","year":"1993","unstructured":"Johnson, N., Kotz, S., Kemp, A.: Univariate Discrete Distributions. Wiley, Hoboken (1993)"},{"key":"12_CR20","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. Ph.D. thesis, RWTH Aachen University, Germany (2019)"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Kaminski, B.L., Katoen, J.: A weakest pre-expectation semantics for mixed-sign expectations. In: ACM\/IEEE Symposium on Logic in Computer Science. LICS, pp. 1\u201312. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005153"},{"issue":"3","key":"12_CR22","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":"12_CR23","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Semantics of probabilistic programs. In: FOCS, pp. 101\u2013114. IEEE Computer Society (1979)","DOI":"10.1109\/SFCS.1979.38"},{"issue":"3","key":"12_CR24","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/0020-0190(82)90065-5","volume":"14","author":"JL Lassez","year":"1982","unstructured":"Lassez, J.L., Nguyen, V.L., Sonenberg, L.: Fixed point theorems and semantics: a folk tale. Inf. Process. Lett. 14(3), 112\u2013116 (1982)","journal-title":"Inf. Process. Lett."},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Monogr. Comput. Sci. Springer (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. In: PACMPL 2(POPL), pp. 33:1\u201333:28 (2018)","DOI":"10.1145\/3158121"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in python. PeerJ Comput. Sci. 3, e103 (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","DOI":"10.7717\/peerj-cs.103"},{"key":"12_CR28","unstructured":"Navarro, A.C.: Order statistics and multivariate discrete phase-type distributions. Ph.D. thesis, DTU Lyngby (2018)"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Neuts, M.F.: Matrix-geometric solutions to stochastic models. In: Steckhan, H., B\u00fchler, W., J\u00e4ger, K.E., Schneewei\u00df, C., Schwarze, J. (eds.) DGOR, pp. 425\u2013425. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/978-3-642-69546-9_91","DOI":"10.1007\/978-3-642-69546-9_91"},{"key":"12_CR30","first-page":"59","volume":"5","author":"D Park","year":"1969","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Mach. Intell. 5, 59\u201378 (1969)","journal-title":"Mach. Intell."},{"key":"12_CR31","doi-asserted-by":"publisher","DOI":"10.1515\/9780691218304","volume-title":"Mathematics and Plausible Reasoning: Induction and Analogy in Mathematics","author":"G P\u00f3lya","year":"1954","unstructured":"P\u00f3lya, G.: Mathematics and Plausible Reasoning: Induction and Analogy in Mathematics. Princeton University Press, Princeton (1954)"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-39519-7_16","volume-title":"Coordination Models and Languages","author":"H Wiklicky","year":"2016","unstructured":"Wiklicky, H.: On dynamical probabilities, or: how to learn to shoot straight. In: Lluch Lafuente, A., Proen\u00e7a, J. (eds.) COORDINATION 2016. LNCS, vol. 9686, pp. 262\u2013277. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-39519-7_16"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-68446-4_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T23:03:54Z","timestamp":1619305434000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-68446-4_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030684457","9783030684464"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-68446-4_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"13 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"LOPSTR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Logic-Based Program Synthesis and Transformation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bologna","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"lopstr2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nms.kcl.ac.uk\/maribel.fernandez\/LOPSTR2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"31","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":"15","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":"0","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":"48% - 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","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":"4","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)"}},{"value":"In addition, two invited talks are included in the proceedings. Due to the COVID-19 pandemic the conference was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}