{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T17:05:16Z","timestamp":1785431116498,"version":"3.56.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","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-nc-nd\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22720-1_12","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:28:14Z","timestamp":1775748494000},"page":"314-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5664-6773","authenticated-orcid":false,"given":"Darion","family":"Haase","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-2176-5075","authenticated-orcid":false,"given":"Adrian","family":"Gallus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","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-0002-3812-0572","authenticated-orcid":false,"given":"Lutz","family":"Klinkenberg","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,4,10]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang. 2(POPL), 34:1\u201334:32 (2018). https:\/\/doi.org\/10.1145\/3158122","DOI":"10.1145\/3158122"},{"key":"12_CR2","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: ESOP. LNCS, vol. 10801, pp. 117\u2013144. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Kov\u00e1cs, L., Stankovic, M.: Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In: ATVA. LNCS, vol. 11781, pp. 255\u2013276. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. In: TACAS. LNCS, vol. 13994, pp. 410\u2013429. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"12_CR5","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. arXiv: 2509.06410","DOI":"10.48550\/ARXIV.2509.06410"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Bauer, C.W., Frink, A., Kreckel, R.B.: Introduction to the GiNaC Framework for Symbolic Computation within the C++ Programming Language. J. Symb. Comput. 33(1), 1\u201312 (2002). https:\/\/doi.org\/10.1006\/jsco.2001.0494. arXiv: cs\/0004015 [cs.SC]","DOI":"10.1006\/jsco.2001.0494"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Beutner, R., Ong, C.L., Zaiser, F.: Guaranteed bounds for posterior inference in universal probabilistic programming. In: PLDI, pp. 536\u2013551. ACM (2022)","DOI":"10.1145\/3519939.3523721"},{"key":"12_CR8","unstructured":"Bingham, E., Chen, J.P., Jankowiak, M., Obermeyer, F., Pradhan, N., Karaletsos, T., Singh, R., Szerlip, P.A., Horsfall, P., Goodman, N.D.: Pyro: Deep Universal Probabilistic Programming. J. Mach. Learn. Res. 20, 28:1\u201328:6 (2019)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bogachev, V.I.: Measure Theory. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-34514-5"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Carpenter, B., Gelman, A., Hoffman, M.D., Lee, D., Goodrich, B., Betancourt, M., Brubaker, M., Guo, J., Li, P., Riddell, A.: Stan: A probabilistic programming language. Journal of statistical software 76, 1\u201332 (2017)","DOI":"10.18637\/jss.v076.i01"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic Program Analysis with Martingales. In: CAV. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"12_CR13","doi-asserted-by":"publisher","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). LNCS, vol. 13371, pp. 79\u2013101. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_5","DOI":"10.1007\/978-3-031-13185-1_5"},{"key":"12_CR14","unstructured":"Chung, K.L.: Markov Chains. Springer, Berlin, Heidelberg (2012)"},{"key":"12_CR15","unstructured":"Collodi, L., Boreale, M., Gregorio, A.P.D.: Towards Algebraic Analysis of Probabilistic Programs. In: ICTCS. CEUR Workshop Proceedings, pp. 147\u2013153. CEURWS. org (2025). https:\/\/ceur-ws.org\/Vol-4039\/paper12.pdf."},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding Polynomial Loop Invariants for Probabilistic Programs. In: ATVA. LNCS, vol. 10482, pp. 400\u2013416. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26","DOI":"10.1007\/978-3-319-68167-2_26"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic Termination: Soundness, Completeness, and Compositionality. In: POPL, pp. 489\u2013501. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Gehr, T., Misailovic, S., Vechev, M.T.: PSI: Exact Symbolic Inference for Probabilistic Programs. In: CAV (1). LNCS, vol. 9779, pp. 62\u201383. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Gei\u00dfler, D., Winkler, T.: Weighted Automata for Exact Inference in Discrete Probabilistic Programs. In: ICTAC. LNCS, vol. 16237, pp. 261\u2013278. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-032-11176-0_16","DOI":"10.1007\/978-3-032-11176-0_16"},{"key":"12_CR20","unstructured":"Goodman, N.D., Stuhlm\u00fcller, A.: The Design and Implementation of Probabilistic Programming Languages, http:\/\/dippl.org (2014). Accessed: 2025-9-30."},{"key":"12_CR21","unstructured":"Goodman, N.D., Tenenbaum, J.B., Contributors, T.P.: Probabilistic Models of Cognition, http:\/\/probmods.org\/ (2016). Accessed: 03\u201305-2025."},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Haase, D., Batz, K., Gallus, A., Kaminski, B.L., Katoen, J.-P., Klinkenberg, L., Winkler, T.: Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops (Extended Version). (2026). https:\/\/doi.org\/10.48550\/arXiv.2601.13991. arXiv: 2601.13991 [cs.PL]","DOI":"10.48550\/arXiv.2601.13991"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Haase, D., Batz, K., Gallus, A., Kaminski, B.L., Katoen, J.-P., Klinkenberg, L., Winkler, T.: Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops: Artifact, (2026). https:\/\/doi.org\/10.5281\/zenodo.18184810","DOI":"10.5281\/zenodo.18184810"},{"key":"12_CR24","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3371105","DOI":"10.1145\/3371105"},{"key":"12_CR25","doi-asserted-by":"publisher","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","DOI":"10.1142\/S012905410200114X"},{"key":"12_CR26","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","DOI":"10.1007\/S10009-021-00633-Z"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: Quicksort. Comput. J. 5(1), 10\u201315 (1962). https:\/\/doi.org\/10.1093\/COMJNL\/5.1.10","DOI":"10.1093\/COMJNL\/5.1.10"},{"key":"12_CR28","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3428208","DOI":"10.1145\/3428208"},{"key":"12_CR29","unstructured":"Kaminski, B.L.: Advanced weakest precondition calculi for probabilistic programs. PhD thesis, RWTH Aachen University, Germany (2019). http:\/\/publications.rwth-aachen.de\/record\/755408"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. In: ESOP. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Katoen, J., McIver, A., Meinicke, L., Morgan, C.C.: Linear-Invariant Generation for Probabilistic Programs: - Automated Support for Proof-Based Methods. In: SAS. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Klinkenberg, L.: Analysis of probabilistic programs using generating functions. Dissertation, RWTH Aachen University, Aachen (2025). https:\/\/doi.org\/10.18154\/RWTH-2025-07571. https:\/\/publications.rwth-aachen.de\/record\/1017915","DOI":"10.18154\/RWTH-2025-07571"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"Klinkenberg, L., Batz, K., Kaminski, B.L., Katoen, J., Moerman, J., Winkler, T.: Generating Functions for Probabilistic Programs. In: LOPSTR. LNCS, vol. 12561, pp. 231\u2013248. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-68446-4_12","DOI":"10.1007\/978-3-030-68446-4_12"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Klinkenberg, L., Blumenthal, C., Chen, M., Haase, D., Katoen, J.: Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. Proc. ACM Program. Lang. 8(OOPSLA1), 923\u2013953 (2024). https:\/\/doi.org\/10.1145\/3649844","DOI":"10.1145\/3649844"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A Probabilistic PDL. J. Comput. Syst. Sci. 30(2), 162\u2013178 (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981). https:\/\/doi.org\/10.1016\/0022-0000(81)90036-2","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"12_CR37","doi-asserted-by":"publisher","unstructured":"Kuich, W.: Semirings and Formal Power Series: Their Relevance to Formal Languages and Automata. In: Handbook of Formal Languages, Volume 1: Word, Language, Grammar. Ed. by G. Rozenberg and A. Salomaa, pp. 609\u2013677. Springer (1997). https:\/\/doi.org\/10.1007\/978-3-642-59136-5_9","DOI":"10.1007\/978-3-642-59136-5_9"},{"key":"12_CR38","doi-asserted-by":"crossref","unstructured":"Lando, S.K.: Lectures on generating functions. American Mathematical Soc. (2003)","DOI":"10.1090\/stml\/023"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"Li, J., Zhang, Y.: Compiling with Generating Functions. Proc. ACM Program. Lang. 9(ICFP) (2025). https:\/\/doi.org\/10.1145\/3747534","DOI":"10.1145\/3747534"},{"key":"12_CR40","unstructured":"Lumbroso, J.O.: Optimal Discrete Uniform Generation from Coin Flips, and Applications. CoRR abs\/1304.1916 (2013). arXiv: 1304.1916. http:\/\/arxiv.org\/abs\/1304.1916"},{"key":"12_CR41","doi-asserted-by":"publisher","unstructured":"Mahdi Shamsi, S., Pietro Farina, G., Gaboardi, M., Napp, N.: Probabilistic Programming Languages for Modeling Autonomous Systems. In: 2020 IEEE International Conference on Multisensor Fusion and Integration for Intelligent Systems (MFI), pp. 32\u201339 (2020). https:\/\/doi.org\/10.1109\/MFI49285.2020.9235230","DOI":"10.1109\/MFI49285.2020.9235230"},{"key":"12_CR42","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"12_CR43","doi-asserted-by":"publisher","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","DOI":"10.1007\/S10817-025-09736-7"},{"key":"12_CR44","doi-asserted-by":"publisher","unstructured":"Meurer, A., Smith, C.P., Paprocki, M., \u010cert\u00edk, O., Kirpichev, S.B., Rocklin, M., Kumar, A., Ivanov, S., Moore, J.K., Singh, S., Rathnayake, T., Vig, S., Granger, B.E., Muller, R.P., Bonazzi, F., Gupta, H., Vats, S., Johansson, F., Pedregosa, F., Curry, M.J., Terrel, A.R., Rou\u010dka, \u0160., Saboo, A., Fernando, I., Kulal, S., Cimrman, R., Scopatz, A.: SymPy: symbolic computing in Python. PeerJ Computer Science 3, e103 (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","DOI":"10.7717\/peerj-cs.103"},{"key":"12_CR45","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Worrell, J.: Positivity Problems for Low-Order Linear Recurrence Sequences. In: SODA, pp. 366\u2013379. SIAM (2014). https:\/\/doi.org\/10.1137\/1.9781611973402.27","DOI":"10.1137\/1.9781611973402.27"},{"key":"12_CR46","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Machine intelligence 5 (1969)"},{"key":"12_CR47","doi-asserted-by":"publisher","unstructured":"Pitman, J.W.: Occupation measures for Markov chains. Advances in Applied Probability 9(1), 69\u201386 (1977). https:\/\/doi.org\/10.2307\/1425817","DOI":"10.2307\/1425817"},{"key":"12_CR48","doi-asserted-by":"publisher","unstructured":"Rabehaja, T.M., Sanders, J.W.: Refinement Algebra with Explicit Probabilism. In: TASE, pp. 63\u201370. IEEE Computer Society (2009). https:\/\/doi.org\/10.1109\/TASE.2009.53","DOI":"10.1109\/TASE.2009.53"},{"key":"12_CR49","doi-asserted-by":"publisher","unstructured":"Sharir, M., Pnueli, A., Hart, S.: Verification of Probabilistic Programs. SIAM J. Comput. 13(2), 292\u2013314 (1984). https:\/\/doi.org\/10.1137\/0213021","DOI":"10.1137\/0213021"},{"key":"12_CR50","doi-asserted-by":"publisher","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and Repulsing Supermartingales for Reachability in Randomized Programs. ACM Trans. Program. Lang. Syst. 43(2), 5:1\u20135:46 (2021). https:\/\/doi.org\/10.1145\/3450967","DOI":"10.1145\/3450967"},{"key":"12_CR51","doi-asserted-by":"publisher","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5(2), 285\u2013309 (1955). https:\/\/doi.org\/10.2140\/pjm.1955.5.285","DOI":"10.2140\/pjm.1955.5.285"},{"key":"12_CR52","doi-asserted-by":"publisher","unstructured":"Torres-Ruiz, M., Piedeleu, R., Silva, A., Zanasi, F.: On Iteration in Discrete Probabilistic Programming. In: FSCD. LIPIcs, 20:1\u201320:21. Schloss Dagstuhl - Leibniz- Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2024.20","DOI":"10.4230\/LIPICS.FSCD.2024.20"},{"key":"12_CR53","unstructured":"Van Rossum, G., Drake, F.L.: Python 3 Reference Manual. CreateSpace, Scotts Valley, CA (2009)"},{"key":"12_CR54","doi-asserted-by":"publisher","unstructured":"Wang, P., Yang, T., Fu, H., Li, G., Ong, C.L.: Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. Proc. ACM Program. Lang. 8(PLDI), 1361\u20131386 (2024). https:\/\/doi.org\/10.1145\/3656432","DOI":"10.1145\/3656432"},{"key":"12_CR55","doi-asserted-by":"crossref","unstructured":"Wilf, H.S.: Generatingfunctionology. A K Peters\/CRC Press (2005).","DOI":"10.1201\/b10576"},{"key":"12_CR56","doi-asserted-by":"publisher","unstructured":"Zaiser, F., Murawski, A.S., Ong, C.L.: Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. Proc. ACM Program. Lang. 9(POPL), 1104\u20131135 (2025). https:\/\/doi.org\/10.1145\/3704874","DOI":"10.1145\/3704874"},{"key":"12_CR57","unstructured":"Zaiser, F., Murawski, A.S., Ong, C.L.: Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach. In: NeurIPS (2023). http:\/\/papers.nips.cc\/paper%5C_files\/paper\/2023\/hash\/0747af6f877c0cb555fea595f01b0e83-Abstract-Conference.html"},{"key":"12_CR58","doi-asserted-by":"publisher","unstructured":"Zhang, L., Zilberstein, N., Kaminski, B.L., Silva, A.: Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers. Proc. ACM Program. Lang. 8(OOPSLA2), 817\u2013845 (2024). https:\/\/doi.org\/10.1145\/3689740","DOI":"10.1145\/3689740"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,30]],"date-time":"2026-07-30T16:39:50Z","timestamp":1785429590000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_12","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":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"A software artifact containing the implementation and benchmark programs described in Section\n                      \n                      is publicly available on Zenodo\u00a0[\n                      \n                      ].","order":1,"name":"Ethics","label":"Data Availability Statement","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","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":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}