{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T09:05:39Z","timestamp":1784797539298,"version":"3.55.0"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325365","type":"print"},{"value":"9783032325372","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,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"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                    is a deductive verifier for probabilistic programs. At its core lies , a quantitative\n                    <jats:italic>intermediate verification language<\/jats:italic>\n                    based on the real-valued logic .  allows users to express a probabilistic program, its specifications, and proof rules in a programming-language style, so that new proof rules can be easily integrated into the verifier.  translates  programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes a backend based on probabilistic model checking for a subset of . We report on the results of five years of development of , highlighting its main features and architecture. In particular, we describe recent improvements such as additional proof rules, a model-checking backend, and better diagnostics.\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-32537-2_27","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:43:55Z","timestamp":1784796235000},"page":"565-582","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Caesar: A Deductive Verifier for\u00a0Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4329-530X","authenticated-orcid":false,"given":"Philipp","family":"Schr\u00f6er","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\/0009-0002-8071-3600","authenticated-orcid":false,"given":"Umut Yi\u011fit","family":"Dural","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5664-6773","authenticated-orcid":false,"given":"Darion","family":"Haase","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-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-81688-9_1","volume-title":"Computer Aided Verification","author":"A Abate","year":"2021","unstructured":"Abate, A., Giacobbe, M., Roy, D.: Learning probabilistic termination proofs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 3\u201326. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_1"},{"key":"27_CR2","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Cohen, C., Saito, A.: Semantics of probabilistic programs using s-finite kernels in dependent type theory. ACM Trans. Probab. Mach. Learn. 1(3) (2025). https:\/\/doi.org\/10.1145\/3732291","DOI":"10.1145\/3732291"},{"key":"27_CR3","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":"27_CR4","doi-asserted-by":"publisher","unstructured":"Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL), 1\u201328 (2021). https:\/\/doi.org\/10.1145\/3434333","DOI":"10.1145\/3434333"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"27_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-031-22308-2_3","volume-title":"Static Analysis - SAS 2022","author":"D Amrollahi","year":"2022","unstructured":"Amrollahi, D., Bartocci, E., Kenison, G., Kov\u00e1cs, L., Moosbrugger, M., Stankovic, M.: Solving invariant generation for unsolvable loops. In: Singh, G., Urban, C. (eds.) SAS 2022. LNCS, vol. 13790, pp. 19\u201343. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-22308-2_3"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"856","DOI":"10.1007\/978-3-030-81685-8_40","volume-title":"Computer Aided Verification","author":"R Andriushchenko","year":"2021","unstructured":"Andriushchenko, R., \u010ce\u0161ka, M., Junges, S., Katoen, J.-P., Stupinsk\u00fd, \u0160: PAYNT: a tool for inductive synthesis of probabilistic programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021, Part I. LNCS, vol. 12759, pp. 856\u2013869. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_40"},{"key":"27_CR8","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 147:1\u2013147:30. ACM (2019). https:\/\/doi.org\/10.1145\/3360573","DOI":"10.1145\/3360573"},{"issue":"OOPSLA1","key":"27_CR9","doi-asserted-by":"publisher","first-page":"784","DOI":"10.1145\/3649839","volume":"8","author":"M Avanzini","year":"2024","unstructured":"Avanzini, M., Barthe, G., Gr\u00e9goire, B., Moser, G., Vanoni, G.: Hopping proofs of expectation-based properties: applications to skiplists and security proofs. Proc. ACM Program. Lang. 8(OOPSLA1), 784\u2013809 (2024). https:\/\/doi.org\/10.1145\/3649839","journal-title":"Proc. ACM Program. Lang."},{"key":"27_CR10","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang. 4(OOPSLA), 172:1\u2013172:30 (2020). https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"27_CR11","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: Automated expected value analysis of recursive programs. Proc. ACM Program. Lang. 7(PLDI), 1050\u20131072 (2023). https:\/\/doi.org\/10.1145\/3591263","DOI":"10.1145\/3591263"},{"key":"27_CR12","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). https:\/\/smt-lib.org"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_3"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-89884-1_5","volume-title":"Programming Languages and Systems","author":"G Barthe","year":"2018","unstructured":"Barthe, G., Espitau, T., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.-Y.: An assertion-based program logic for probabilistic programs. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 117\u2013144. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_5"},{"key":"27_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-031-30820-8_25","volume-title":"TACAS 2023","author":"K Batz","year":"2023","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 2023. LNCS, vol. 13994, pp. 410\u2013429. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_25"},{"key":"27_CR17","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,Part II. LNCS, vol. 12760, pp. 524\u2013549. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_25"},{"key":"27_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/978-3-030-53291-8_27","volume-title":"Computer Aided Verification","author":"K Batz","year":"2020","unstructured":"Batz, K., Junges, S., Kaminski, B.L., Katoen, J.-P., Matheja, C., Schr\u00f6er, P.: PrIC3: property directed reachability for MDPs. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 512\u2013538. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_27"},{"key":"27_CR19","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. Proc. ACM Program. Lang. 5(POPL), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3434320","DOI":"10.1145\/3434320"},{"issue":"OOPSLA1","key":"27_CR20","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1145\/3720429","volume":"9","author":"K Batz","year":"2025","unstructured":"Batz, K., Katoen, J., Randone, F., Winkler, T.: Foundations for deductive verification of continuous probabilistic programs: from Lebesgue to Riemann and back. Proc. ACM Program. Lang. 9(OOPSLA1), 421\u2013448 (2025). https:\/\/doi.org\/10.1145\/3720429","journal-title":"Proc. ACM Program. Lang."},{"key":"27_CR21","doi-asserted-by":"publisher","unstructured":"Beothy-Elo, E.: Effective quantifier-based reasoning for quantitative deductive verification. MA thesis, RWTH Aachen University, Aachen (2025). https:\/\/doi.org\/10.18154\/RWTH-2025-07050, https:\/\/publications.rwth-aachen.de\/record\/1016969","DOI":"10.18154\/RWTH-2025-07050"},{"key":"27_CR22","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., et al.: Learning algorithms for verification of markov decision processes. TheoretiCS 4 (2025). https:\/\/doi.org\/10.46298\/THEORETICS.25.10","DOI":"10.46298\/THEORETICS.25.10"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-662-54580-5_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"CE Budde","year":"2017","unstructured":"Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017, Part II. LNCS, vol. 10206, pp. 151\u2013168. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_9"},{"key":"27_CR24","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":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1007\/978-3-319-21690-4_44","volume-title":"Computer Aided Verification","author":"Y-F Chen","year":"2015","unstructured":"Chen, Y.-F., Hong, C.-D., Wang, B.-Y., Zhang, L.: Counterexample-guided polynomial loop invariant generation by Lagrange interpolation. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 658\u2013674. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_44"},{"key":"27_CR26","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/BFB0035403","volume-title":"Tools and Algorithms for Construction and Analysis of Systems - TACAS \u201997","author":"PR D\u2019Argenio","year":"1997","unstructured":"D\u2019Argenio, P.R., Katoen, J., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time! In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416\u2013431. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFB0035403"},{"key":"27_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"27_CR28","doi-asserted-by":"publisher","unstructured":"Enea, C., Majumdar, R., Motwani, H.J., Sathiyanarayana, V.R.: Verifying almost-sure termination for randomized distributed algorithms. Proc. ACM Program. Lang. 10(POPL) (2026). https:\/\/doi.org\/10.1145\/3776691","DOI":"10.1145\/3776691"},{"issue":"OOPSLA1","key":"27_CR29","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1145\/3586051","volume":"7","author":"S Feng","year":"2023","unstructured":"Feng, S., Chen, M., Su, H., Kaminski, B.L., Katoen, J., Zhan, N.: Lower bounds for possibly divergent probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA1), 696\u2013726 (2023). https:\/\/doi.org\/10.1145\/3586051","journal-title":"Proc. ACM Program. Lang."},{"key":"27_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/978-3-319-68167-2_26","volume-title":"Automated Technology for Verification and Analysis","author":"Y Feng","year":"2017","unstructured":"Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding polynomial loop invariants for probabilistic programs. In: D\u2019Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 400\u2013416. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68167-2_26"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"27_CR32","doi-asserted-by":"publisher","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15\u201317 January 2015, pp. 489\u2013501. ACM (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"27_CR33","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, Part I. LNCS, vol. 9779, pp. 62\u201383. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_4"},{"key":"27_CR34","doi-asserted-by":"publisher","unstructured":"Haase, D., et al.: Generating functions meet occupation measures: invariant synthesis for probabilistic loops. In: Krebbers, R. (ed.) ESOP 2026, ETAPS 2026, Part I. LNCS, pp. 314\u2013343. Springer, Heidelberg (2026). https:\/\/doi.org\/10.1007\/978-3-032-22720-1_12","DOI":"10.1007\/978-3-032-22720-1_12"},{"key":"27_CR35","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R.: Dijkstra\u2019s legacy on program verification. In: Apt, K.R., Hoare, T. (eds.) Edsger Wybe Dijkstra: His Life, Work, and Legacy, pp. 105\u2013140. ACM\/Morgan & Claypool (2022). https:\/\/doi.org\/10.1145\/3544585.3544593","DOI":"10.1145\/3544585.3544593"},{"key":"27_CR36","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"},{"issue":"4","key":"27_CR37","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). https:\/\/doi.org\/10.1007\/S10009-021-00633-Z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"27_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-319-43144-4_30","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2016","unstructured":"H\u00f6lzl, J.: Formalising semantics for expected running time of probabilistic programs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 475\u2013482. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_30"},{"key":"27_CR39","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"},{"issue":"1","key":"27_CR40","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theoret. Comput. Sci. 346(1), 96\u2013112 (2005). https:\/\/doi.org\/10.1016\/j.tcs.2005.08.005","journal-title":"Theoret. Comput. Sci."},{"key":"27_CR41","unstructured":"Jaarsveld, F.v.: Practical Probabilistic Program Verification using Caesar. Thesis, University of Twente, Enschede (2025). https:\/\/purl.utwente.nl\/essays\/106318"},{"key":"27_CR42","unstructured":"Jones, C.: Probabilistic non-determinism. Ph.D. thesis, University of Edinburgh, UK (1990). https:\/\/hdl.handle.net\/1842\/413"},{"key":"27_CR43","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L.: Advanced Weakest Precondition Calculi for Probabilistic Programs. Ph.D. thesis, RWTH Aachen University (2019). https:\/\/doi.org\/10.18154\/RWTH-2019-01829","DOI":"10.18154\/RWTH-2019-01829"},{"issue":"3","key":"27_CR44","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/S00236-018-0321-1","volume":"56","author":"BL Kaminski","year":"2019","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Informatica 56(3), 255\u2013285 (2019). https:\/\/doi.org\/10.1007\/S00236-018-0321-1","journal-title":"Acta Informatica"},{"key":"27_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run\u2013times of probabilistic programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15"},{"key":"27_CR46","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"27_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs: - automated support for proof-based methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"key":"27_CR48","doi-asserted-by":"publisher","unstructured":"Kawamoto, Y., Kobayashi, K., Suenaga, K.: StatWhy: formal verification tool for statistical hypothesis testing programs. In: Piskac, R., Rakamaric, Z. (eds.) CAV 2025, Part II. LNCS, pp. 216\u2013230. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-031-98679-6_10","DOI":"10.1007\/978-3-031-98679-6_10"},{"issue":"3","key":"27_CR49","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/S00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Asp. Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/S00165-014-0326-7","journal-title":"Formal Asp. Comput."},{"key":"27_CR50","doi-asserted-by":"publisher","unstructured":"Kozen, D.: A probabilistic PDL. In: STOC, pp. 291\u2013297. ACM (1983). https:\/\/doi.org\/10.1145\/800061.808758","DOI":"10.1145\/800061.808758"},{"issue":"2","key":"27_CR51","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). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","journal-title":"J. Comput. Syst. Sci."},{"key":"27_CR52","doi-asserted-by":"publisher","unstructured":"Kushilevitz, E., Rabin, M.O.: Randomized mutual exclusion algorithms revisited. In: Hutchinson, N.C. (ed.) Proceedings of the Eleventh Annual ACM Symposium on Principles of Distributed Computing, Vancouver, British Columbia, Canada, 10\u201312 August 1992, pp. 275\u2013283. ACM (1992). https:\/\/doi.org\/10.1145\/135419.135468","DOI":"10.1145\/135419.135468"},{"key":"27_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"27_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"27_CR55","unstructured":"Leino, K.R.M.: This is Boogie 2 (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"27_CR56","doi-asserted-by":"publisher","unstructured":"Leutgeb, L., Moser, G., Zuleger, F.: Automated expected amortised cost analysis of probabilistic data structures. In: CAV 2022. LNCS, vol. 13372, pp. 70\u201391. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_4","DOI":"10.1007\/978-3-031-13188-2_4"},{"key":"27_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-38171-3_11","volume-title":"Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems","author":"MH Liffiton","year":"2013","unstructured":"Liffiton, M.H., Malik, A.: Enumerating infeasibility: finding multiple MUSes quickly. In: Gomes, C., Sellmann, M. (eds.) CPAIOR 2013. LNCS, vol. 7874, pp. 160\u2013175. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38171-3_11"},{"key":"27_CR58","doi-asserted-by":"publisher","unstructured":"Majumdar, R., Sathiyanarayana, V.R.: Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang. 9(POPL), 1871\u20131902 (2025). https:\/\/doi.org\/10.1145\/3704899","DOI":"10.1145\/3704899"},{"key":"27_CR59","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-031-75434-0_17","volume-title":"Bridging the Gap Between AI and Reality - AISoLA 2024","author":"C Matheja","year":"2024","unstructured":"Matheja, C.: A game-based semantics for the probabilistic intermediate verification language HeyVL. In: Steffen, B. (ed.) AISoLA 2024. LNCS, vol. 15217, pp. 242\u2013258. Springer, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-75434-0_17"},{"key":"27_CR60","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almostsure termination. Proc. ACM Program. Lang. 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"27_CR61","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York (2005)","DOI":"10.1145\/1059816.1059824"},{"key":"27_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-72016-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Meyer","year":"2021","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021, Part I. LNCS, vol. 12651, pp. 250\u2013269. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14"},{"key":"27_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-72019-3_18","volume-title":"Programming Languages and Systems","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP 2021. LNCS, vol. 12648, pp. 491\u2013518. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18"},{"key":"27_CR64","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"},{"issue":"OOPSLA2","key":"27_CR65","doi-asserted-by":"publisher","first-page":"1497","DOI":"10.1145\/3563341","volume":"6","author":"M Moosbrugger","year":"2022","unstructured":"Moosbrugger, M., Stankovic, M., Bartocci, E., Kov\u00e1cs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang. 6(OOPSLA2), 1497\u20131525 (2022). https:\/\/doi.org\/10.1145\/3563341","journal-title":"Proc. ACM Program. Lang."},{"key":"27_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"27_CR67","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI 2018. Association for Computing Machinery, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"key":"27_CR68","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. Springer, Cham (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"27_CR69","doi-asserted-by":"publisher","unstructured":"Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J., McIver, A.: Conditioning in probabilistic programming. ACM Trans. Program. Lang. Syst. 40(1), 4:1\u20134:50 (2018). https:\/\/doi.org\/10.1145\/3156018","DOI":"10.1145\/3156018"},{"key":"27_CR70","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. Mach. Intell. 5 (1969)"},{"key":"27_CR71","doi-asserted-by":"publisher","unstructured":"Schroer, P.: A deductive verifier for probabilistic programs. MA thesis, RWTH Aachen University, Aachen (2024). https:\/\/doi.org\/10.18154\/RWTH-2024-11340, https:\/\/publications.rwth-aachen.de\/record\/998370","DOI":"10.18154\/RWTH-2024-11340"},{"key":"27_CR72","doi-asserted-by":"publisher","unstructured":"Schr\u00f6er, P., et al.: Caesar: A Deductive Verifier for Probabilistic Programs (CAV26 Artifact). Zenodo (2026). https:\/\/doi.org\/10.5281\/zenodo.19838026","DOI":"10.5281\/zenodo.19838026"},{"issue":"OOPSLA2","key":"27_CR73","doi-asserted-by":"publisher","first-page":"2052","DOI":"10.1145\/3622870","volume":"7","author":"P Schr\u00f6er","year":"2023","unstructured":"Schr\u00f6er, P., Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: A deductive verification infrastructure for probabilistic programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052\u20132082 (2023). https:\/\/doi.org\/10.1145\/3622870","journal-title":"Proc. ACM Program. Lang."},{"key":"27_CR74","doi-asserted-by":"publisher","unstructured":"Schr\u00f6er, P., Haase, D., Katoen, J.: Error localization, certificates, and hints for probabilistic program verification via slicing. In: Krebbers, R. (ed.) Programming Languages and Systems - ESOP 2026, ETAPS 2026, Part II. LNCS, pp. 210\u2013240. Springer, Heidelberg (2026). https:\/\/doi.org\/10.1007\/978-3-032-22723-2_8","DOI":"10.1007\/978-3-032-22723-2_8"},{"key":"27_CR75","doi-asserted-by":"crossref","unstructured":"Schr\u00f6er, P., Katoen, J.: Highly incremental: a simple programmatic approach for many objectives. In: Formal Methods - 27th International Symposium, FM 2026. LNCS, Springer, Heidelberg (2026)","DOI":"10.1007\/978-3-032-26204-2_29"},{"key":"27_CR76","doi-asserted-by":"publisher","unstructured":"Tristan, J.-B.: SampCert: Verified Differential Privacy, version 1.0.0. (2024). https:\/\/doi.org\/10.5281\/zenodo.11204806, https:\/\/github.com\/leanprover\/SampCert","DOI":"10.5281\/zenodo.11204806"},{"key":"27_CR77","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":"27_CR78","unstructured":"Zetzsche, S., Tristan, J.-B.: Dafny-VMC: a Library for Verified Monte Carlo Algorithms, Software (2023). https:\/\/github.com\/dafny-lang\/Dafny-VMC"}],"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-032-32537-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:44:02Z","timestamp":1784796242000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32537-2_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325365","9783032325372"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32537-2_27","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":"24 July 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","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"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":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}