pith. sign in

arxiv: 2605.15827 · v1 · pith:M63EQNBFnew · submitted 2026-05-15 · 💻 cs.PL

Caesar: A Deductive Verifier for Probabilistic Programs

Philipp Schr\"oer , Kevin Batz , Umut Yi\u{g}it Dural , Darion Haase , Benjamin Lucien Kaminski , Joost-Pieter Katoen , Christoph Matheja This is my paper

Pith reviewed 2026-05-19 18:09 UTC · model grok-4.3

classification 💻 cs.PL
keywords deductive verificationprobabilistic programsintermediate verification languageHeyVLSMT solvingmodel checkingquantitative specifications
0
0 comments X

The pith

Caesar translates HeyVL programs for probabilistic programs into verification conditions checked by Z3.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Caesar as a deductive verifier that lets users write probabilistic programs along with their specifications and custom proof rules in a programming-language style. These descriptions are expressed in HeyVL, an intermediate language built on the real-valued logic HeyLo, and then turned into verification conditions. The conditions are passed to the Z3 SMT solver for checking, while a separate probabilistic model-checking backend handles a restricted subset of programs. A reader would care because this setup makes it straightforward to incorporate new proof rules and to verify programs whose behavior involves randomness, a class of systems that standard deductive tools do not directly address.

Core claim

Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL 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. Caesar translates HeyVL 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 HeyVL.

What carries the argument

HeyVL, the quantitative intermediate verification language based on HeyLo, which encodes a probabilistic program, its specifications, and user-supplied proof rules for translation into solver-ready conditions.

If this is right

  • New proof rules can be added by writing them directly in the programming-language style of HeyVL rather than modifying the verifier core.
  • Verification conditions for general HeyVL programs are discharged by the Z3 SMT solver.
  • A subset of HeyVL programs can be handled by a dedicated probabilistic model-checking backend.
  • Diagnostic information is improved to help users understand why a verification attempt succeeds or fails.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The extensible rule mechanism could support verification of randomized algorithms in domains such as cryptography or distributed systems where custom quantitative invariants are needed.
  • Hybrid use of the model-checking backend and the SMT backend might reduce the number of cases that require manual proof-rule invention.
  • The five-year development history suggests that incremental addition of rules and diagnostics can turn a research prototype into a tool usable on realistic examples.

Load-bearing premise

The HeyLo logic together with the added proof rules is sound and Z3 can decide the verification conditions that arise from the intended class of probabilistic programs.

What would settle it

A probabilistic program that is known to violate its stated specification yet receives a successful verification result from Caesar would show that the translation or the underlying logic fails to preserve correctness.

Figures

Figures reproduced from arXiv: 2605.15827 by Benjamin Lucien Kaminski, Christoph Matheja, Darion Haase, Joost-Pieter Katoen, Kevin Batz, Philipp Schr\"oer, Umut Yi\u{g}it Dural.

Figure 1
Figure 1. Figure 1: Excerpt of HeyVL code modeling the bounded retransmission protocol. maxTries attempts per packet before aborting. The program is written in HeyVL, a quantitative verification-aware programming language, explained below. Design and verification objectives for probabilistic programs go beyond clas￾sical safety and liveness, and are quantitative rather than Boolean. For the BRP, one may bound the failure prob… view at source ↗
Figure 2
Figure 2. Figure 2: Logical architecture of the Caesar verifier [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Overview of which approximation of the reference semantics to use when [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Caesar’s VSCode extension providing diagnostics and explanations. and counterexamples can be semantically spurious. Caesar’s UI/UX is designed to make these issues explicit, guide users away from unsound reasoning, and shorten the verification feedback loop. Features are explained in detail in the extensive documentation10 . 5.1 Installation and Command-Line Interface Caesar is distributed as a single bina… view at source ↗
read the original abstract

Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL 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. Caesar translates HeyVL 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 HeyVL. We report on the results of five years of development of Caesar, highlighting its main features and architecture. In particular, we describe recent improvements such as additional proof rules, a model-checking backend, and better diagnostics.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper presents Caesar, a deductive verifier for probabilistic programs. At its core is HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL allows users to express probabilistic programs, specifications, and proof rules in a programming-language style. Caesar translates HeyVL programs into verification conditions checked by the Z3 SMT solver and includes a probabilistic model-checking backend for a subset of HeyVL. The manuscript reports on five years of development, highlighting the architecture, new proof rules, the model-checking backend, and improved diagnostics.

Significance. If the described translation and features function as claimed, this work provides a practical, extensible tool for deductive verification of probabilistic programs. The programming-language-style integration of proof rules and the dual-backend approach (SMT plus model checking) are notable strengths for usability in the field. The five-year development effort with concrete additions like new rules and diagnostics represents a substantial engineering contribution that could support further research in probabilistic verification.

minor comments (3)
  1. The abstract and introduction would benefit from one or two concrete examples of a HeyVL program, its specification, and the generated verification condition to illustrate the translation process.
  2. The manuscript should clarify the scope of the model-checking backend (e.g., which fragment of HeyVL it supports) and any performance trade-offs relative to the Z3 path.
  3. A short discussion of limitations, such as the class of programs for which Z3 decides the VCs in practice, would strengthen the presentation.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive and constructive review of our manuscript on Caesar. We appreciate the recognition of the practical value of HeyVL for integrating proof rules in a programming-language style, the dual SMT and model-checking backends, and the five-year engineering effort. The referee's summary accurately reflects the paper's contributions. Since no specific major comments were raised in the report, we have no point-by-point revisions to address at this stage. We remain available to incorporate any minor suggestions or clarifications that may be provided.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper is a system-description report on the Caesar verifier. Its central claims concern the architecture of translating HeyVL programs (based on the external HeyLo logic) into Z3-checkable verification conditions plus a model-checking backend for a subset. These are implementation and engineering results resting on external solvers and the soundness of the underlying logic, which the paper does not derive internally. No equations, predictions, or proof steps reduce by construction to fitted parameters or self-referential definitions. Self-citations, if present for prior HeyLo work, are not load-bearing for the reported tool features and are externally falsifiable via the implemented system.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The verifier rests on the soundness of the HeyLo quantitative logic and the completeness of the translation to Z3; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • domain assumption HeyLo is a sound real-valued logic for probabilistic programs and the added proof rules preserve this soundness.
    The entire verification pipeline depends on this background property of the logic.

pith-pipeline@v0.9.0 · 5675 in / 1140 out tokens · 39433 ms · 2026-05-19T18:09:23.901020+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

74 extracted references · 74 canonical work pages

  1. [1]

    In: Silva, A., Leino, K.R.M

    Abate, A., Giacobbe, M., Roy, D.: Learning Probabilistic Termination Proofs. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd Interna- tional Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II. LNCS, vol. 12760, pp. 3–26. Springer, Heidelberg (2021).https://doi.org/ 10.1007/978-3-030-81688-9_1

    work page doi:10.1007/978-3-030-81688-9_1 2021

  2. [2]

    ACM Trans

    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

    work page doi:10.1145/3732291 2025

  3. [3]

    Agrawal, S., Chatterjee, K., Novotn´ y, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Pro- gram. Lang.2(POPL), 34:1–34:32 (2018).https://doi.org/10.1145/3158122

    work page doi:10.1145/3158122 2018

  4. [4]

    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–28 (2021).https://doi.org/10.1145/3434333

    work page doi:10.1145/3434333 2021

  5. [5]

    (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice

    Ahrendt, W., Beckert, B., Bubel, R., H¨ ahnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. Springer (2016)

    work page 2016

  6. [6]

    In: Singh, G., Urban, C

    Amrollahi, D., Bartocci, E., Kenison, G., Kov´ acs, L., Moosbrugger, M., Stankovic, M.: Solving Invariant Generation for Unsolvable Loops. In: Singh, G., Urban, C. (eds.) Static Analysis - 29th International Symposium, SAS 2022, Auckland, New Zealand, December 5-7, 2022, Proceedings. LNCS, vol. 13790, pp. 19–43. Springer, Heidelberg (2022).https://doi.org...

    work page doi:10.1007/978-3-031-22308-2_3 2022

  7. [7]

    In: Silva, A., Leino, K.R.M

    Andriushchenko, R., Ceska, M., Junges, S., Katoen, J., Stupinsk´ y, S.: PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I. LNCS, pp. 856–869. Springer, Heidelberg (2021).https://doi....

    work page doi:10.1007/978-3-030-81685-8_40 2021

  8. [8]

    In: Object-Oriented Programming Sys- tems, Languages, and Applications (OOPSLA), 147:1–147:30

    Astrauskas, V., M¨ uller, P., Poli, F., Summers, A.J.: Leveraging Rust Types for Modular Specification and Verification. In: Object-Oriented Programming Sys- tems, Languages, and Applications (OOPSLA), 147:1–147:30. ACM (2019).https: //doi.org/10.1145/3360573 14 P. Schr¨ oer et al

    work page doi:10.1145/3360573 2019

  9. [9]

    Avanzini, M., Barthe, G., Gr´ egoire, B., Moser, G., Vanoni, G.: Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang.8(OOPSLA1), 784–809 (2024).https://doi.org/10.1145/ 3649839

    work page 2024

  10. [10]

    Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang.4(OOPSLA), 172:1–172:30 (2020).https: //doi.org/10.1145/3428240

    work page doi:10.1145/3428240 2020

  11. [11]

    Avanzini, M., Moser, G., Schaper, M.: Automated Expected Value Analysis of Re- cursive Programs. Proc. ACM Program. Lang.7(PLDI), 1050–1072 (2023).https: //doi.org/10.1145/3591263

    work page doi:10.1145/3591263 2023

  12. [12]

    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB), (2016).https://smt-lib.org

    work page 2016

  13. [14]

    In: Chaudhuri, S., Farzan, A

    Barthe, G., Espitau, T., Fioriti, L.M.F., Hsu, J.: Synthesizing Probabilistic In- variants via Doob’s Decomposition. In: Chaudhuri, S., Farzan, A. (eds.) Com- puter Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. LNCS, vol. 9779, pp. 43–61. Springer, Heidelberg (2016).https://doi.or...

    work page doi:10.1007/978-3-319-41528-4_3 2016

  14. [16]

    In: TACAS (2)

    Batz, K., Chen, M., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C.: Prob- abilistic Program Verification via Inductive Synthesis of Inductive Invariants. In: TACAS (2). LNCS, vol. 13994, pp. 410–429. Springer, Heidelberg (2023).https: //doi.org/10.1007/978-3-031-30820-8_25

    work page doi:10.1007/978-3-031-30820-8_25 2023

  15. [18]

    In: CAV (2)

    Batz, K., Junges, S., Kaminski, B.L., Katoen, J., Matheja, C., Schr¨ oer, P.: PrIC3: Property Directed Reachability for MDPs. In: CAV (2). LNCS, vol. 12225, pp. 512–

    work page

  16. [19]

    Springer, Heidelberg (2020).https://doi.org/10.1007/978-3-030-53291- 8_27

    work page doi:10.1007/978-3-030-53291- 2020

  17. [20]

    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–30 (2021).https://doi.org/10.1145/ 3434320

    work page 2021

  18. [21]

    Batz, K., Katoen, J., Randone, F., Winkler, T.: Foundations for Deductive Ver- ification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Caesar15 Back. Proc. ACM Program. Lang.9(OOPSLA1), 421–448 (2025).https://doi. org/10.1145/3720429

    work page doi:10.1145/3720429 2025

  19. [22]

    MA thesis, RWTH Aachen University, Aachen (2025).https://doi.org/ 10.18154/RWTH-2025-07050.https://publications.rwth-aachen.de/record/ 1016969

    Beothy-Elo, E.: Effective quantifier-based reasoning for quantitative deductive ver- ification. MA thesis, RWTH Aachen University, Aachen (2025).https://doi.org/ 10.18154/RWTH-2025-07050.https://publications.rwth-aachen.de/record/ 1016969

    work page doi:10.18154/rwth-2025-07050.https://publications.rwth-aachen.de/record/ 2025

  20. [23]

    TheoretiCS4(2025).https://doi.org/10.46298/ THEORETICS.25.10

    Br´ azdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kret´ ınsk´ y, J., Kwiatkowska, M., Meggendorfer, T., Parker, D., Ujma, M.: Learning Algorithms for Verification of Markov Decision Processes. TheoretiCS4(2025).https://doi.org/10.46298/ THEORETICS.25.10

    work page 2025

  21. [24]

    In: Legay, A., Margaria, T

    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.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd Interna- tional Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, E...

    work page doi:10.1007/978-3-662-54580-5_9 2017

  22. [25]

    In: Sharygina, N., Veith, H

    Chakarov, A., Sankaranarayanan, S.: Probabilistic Program Analysis with Mar- tingales. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. LNCS, vol. 8044, pp. 511–526. Springer, Heidelberg (2013).https: //doi.org/10.1007/978-3-642-39799-8_34

    work page doi:10.1007/978-3-642-39799-8_34 2013

  23. [26]

    In: Kroening, D., Pasare- anu, C.S

    Chen, Y., Hong, C., Wang, B., Zhang, L.: Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation. In: Kroening, D., Pasare- anu, C.S. (eds.) Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. LNCS, vol. 9206, pp. 658–674. Springer, Heidelberg (2...

    work page 2015

  24. [27]

    (ed.) Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS ’97, Enschede, The Netherlands, April 2-4, 1997, Proceedings

    D’Argenio, P.R., Katoen, J., Ruys, T.C., Tretmans, J.: The Bounded Retrans- mission Protocol Must Be on Time! In: Brinksma, E. (ed.) Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS ’97, Enschede, The Netherlands, April 2-4, 1997, Proceedings. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997).https...

    work page doi:10.1007/bfb0035403 1997

  25. [28]

    Z3 : An efficient SMT solver

    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2008).https: //doi.org/10.1007/978-3-540-78800-3_24

    work page doi:10.1007/978-3-540-78800-3_24 2008

  26. [29]

    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

    work page doi:10.1145/3776691 2026

  27. [30]

    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–726 (2023).https://doi.org/10.1145/3586051

    work page doi:10.1145/3586051 2023

  28. [31]

    In: D’Souza, D., Kumar, K.N

    Feng, Y., Zhang, L., Jansen, D.N., Zhan, N., Xia, B.: Finding Polynomial Loop Invariants for Probabilistic Programs. In: D’Souza, D., Kumar, K.N. (eds.) Au- tomated Technology for Verification and Analysis - 15th International Sympo- sium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings. LNCS, vol. 10482, pp. 400–416. Springer, Heidelberg (2017).ht...

    work page doi:10.1007/978-3-319- 2017

  29. [32]

    In: ESOP

    Filliˆ atre, J., Paskevich, A.: Why3 - Where Programs Meet Provers. In: ESOP. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013).https://doi.org/10. 1007/978-3-642-37036-6_8

    work page 2013

  30. [33]

    In: Rajamani, S.K., Walker, D

    Fioriti, L.M.F., Hermanns, H.: Probabilistic Termination: Soundness, Complete- ness, and Compositionality. In: Rajamani, S.K., Walker, D. (eds.) Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Program- ming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pp. 489–501. ACM (2015).https://doi.org/10.1145/2676726.2677001

    work page doi:10.1145/2676726.2677001 2015

  31. [34]

    In: Chaudhuri, S., Farzan, A

    Gehr, T., Misailovic, S., Vechev, M.T.: PSI: Exact Symbolic Inference for Prob- abilistic Programs. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verifi- cation - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. LNCS, pp. 62–83. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-41528-4_4

    work page doi:10.1007/978-3-319-41528-4_4 2016

  32. [35]

    In: Krebbers, R

    Haase, D., Batz, K., Gallus, A., Kaminski, B.L., Katoen, J., Klinkenberg, L., Win- kler, T.: Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops. In: Krebbers, R. (ed.) Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory ...

    work page doi:10.1007/978-3-032-22720-1_12 2026

  33. [36]

    In: Edsger Wybe Dijkstra: His Life, Work, and Legacy

    H¨ ahnle, R.: Dijkstra’s Legacy on Program Verification. In: Edsger Wybe Dijkstra: His Life, Work, and Legacy. Ed. by K.R. Apt and T. Hoare, pp. 105–140. ACM / Morgan & Claypool (2022).https://doi.org/10.1145/3544585.3544593

    work page doi:10.1145/3544585.3544593 2022

  34. [37]

    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–37:28 (2020).https://doi.org/10.1145/3371105

    work page doi:10.1145/3371105 2020

  35. [38]

    Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transf.24(4), 589–610 (2022). https://doi.org/10.1007/S10009-021-00633-Z

    work page doi:10.1007/s10009-021-00633-z 2022

  36. [39]

    In: Blanchette, J.C., Merz, S

    H¨ olzl, J.: Formalising Semantics for Expected Running Time of Probabilistic Pro- grams. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceed- ings. LNCS, vol. 9807, pp. 475–482. Springer, Heidelberg (2016).https://doi. org/10.1007/978-3-319-43144-4_30

    work page doi:10.1007/978-3-319-43144-4_30 2016

  37. [40]

    In: Hou, Z., Ganesh, V

    Huang, Z., Dutta, S., Misailovic, S.: AQUA: Automated Quantized Inference for Probabilistic Programs. In: Hou, Z., Ganesh, V. (eds.) Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings. LNCS, pp. 229–246. Springer, Heidelberg (2021).https://doi.org/10.10...

    work page doi:10.1007/978-3-030-88885-5_16 2021

  38. [41]

    Theoretical Computer Science346(1), 96–112 (2005).https://doi.org/ 10.1016/j.tcs.2005.08.005

    Hurd, J., McIver, A., Morgan, C.: Probabilistic Guarded Commands Mechanized in HOL. Theoretical Computer Science346(1), 96–112 (2005).https://doi.org/ 10.1016/j.tcs.2005.08.005

    work page doi:10.1016/j.tcs.2005.08.005 2005

  39. [42]

    Thesis, University of Twente, Enschede (2025).https : / / purl

    Jaarsveld, F.v.: Practical Probabilistic Program Verification using Caesar. Thesis, University of Twente, Enschede (2025).https : / / purl . utwente . nl / essays / 106318

    work page 2025

  40. [43]

    PhD thesis, University of Edinburgh, UK (1990).https://hdl.handle.net/1842/413

    Jones, C.: Probabilistic non-determinism. PhD thesis, University of Edinburgh, UK (1990).https://hdl.handle.net/1842/413

    work page 1990

  41. [44]

    PhD thesis, RWTH Aachen University (2019).https : / / doi

    Kaminski, B.L.: Advanced Weakest Precondition Calculi for Probabilistic Pro- grams. PhD thesis, RWTH Aachen University (2019).https : / / doi . org / 10 . 18154/RWTH-2019-01829. Caesar17

    work page 2019

  42. [45]

    Acta Informatica56(3), 255–285 (2019).https://doi.org/10.1007/ S00236-018-0321-1

    Kaminski, B.L., Katoen, J., Matheja, C.: On the hardness of analyzing probabilistic programs. Acta Informatica56(3), 255–285 (2019).https://doi.org/10.1007/ S00236-018-0321-1

    work page 2019

  43. [46]

    In: Thiemann, P

    Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs. In: Thiemann, P. (ed.) Programming Languages and Systems. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2016).https : / / doi . org / 10 . 1007 / 978 - 3 - 662 - 49498-1_15

    work page 2016

  44. [47]

    Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest Precondition Rea- soning for Expected Runtimes of Randomized Algorithms. J. ACM65(5), 30:1– 30:68 (2018).https://doi.org/10.1145/3208102

    work page doi:10.1145/3208102 2018

  45. [49]

    In: Piskac, R., Rakamaric, Z

    Kawamoto, Y., Kobayashi, K., Suenaga, K.: StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part II. LNCS, pp. 216–230. Springer, Heidelberg (2025).https://doi.org/10.1007/...

    work page doi:10.1007/978-3-031-98679-6_10 2025

  46. [50]

    Formal Aspects Comput.27(3), 573–609 (2015)

    Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. Formal Aspects Comput.27(3), 573–609 (2015). https://doi.org/10.1007/S00165-014-0326-7

    work page doi:10.1007/s00165-014-0326-7 2015

  47. [51]

    In: STOC, pp

    Kozen, D.: A Probabilistic PDL. In: STOC, pp. 291–297. ACM (1983).https : //doi.org/10.1145/800061.808758

    work page doi:10.1145/800061.808758 1983

  48. [52]

    Kozen, D.: A Probabilistic PDL. J. Comput. Syst. Sci.30(2), 162–178 (1985). https://doi.org/10.1016/0022-0000(85)90012-1

    work page doi:10.1016/0022-0000(85)90012-1 1985

  49. [53]

    In: Hutchinson, N.C

    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, August 10-12, 1992, pp. 275–283. ACM (1992).https : / / doi . org / 10 . 1145 / 135419.135468

    work page arXiv 1992

  50. [54]

    In: Gopalakrishnan, G., Qadeer, S

    Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of Proba- bilistic Real-Time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. LNCS, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47

    work page doi:10.1007/978-3-642-22110-1_47 2011

  51. [55]

    In: Clarke, E.M., Voronkov, A

    Leino, K.R.M.: Dafny: An Automatic Program Verifier for Functional Correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science. Springer, Berlin, Heidelberg (2010).https://doi.org/10.1007/978-3-642-17511-4_20

    work page doi:10.1007/978-3-642-17511-4_20 2010

  52. [56]

    microsoft

    Leino, K.R.M.: This is Boogie 2, (2008).https : / / www . microsoft . com / en - us/research/publication/this-is-boogie-2-2/

    work page 2008

  53. [57]

    In: CAV (2)

    Leutgeb, L., Moser, G., Zuleger, F.: Automated Expected Amortised Cost Anal- ysis of Probabilistic Data Structures. In: CAV (2). LNCS, vol. 13372, pp. 70–91. Springer, Heidelberg (2022).https://doi.org/10.1007/978-3-031-13188-2_4

    work page doi:10.1007/978-3-031-13188-2_4 2022

  54. [58]

    In: Gomes, C.P., Sellmann, M

    Liffiton, M.H., Malik, A.: Enumerating Infeasibility: Finding Multiple MUSes Quickly. In: Gomes, C.P., Sellmann, M. (eds.) Integration of AI and OR Techniques in 18 P. Schr¨ oer et al. Constraint Programming for Combinatorial Optimization Problems, 10th Interna- tional Conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18-22, 2013. Proceedings. LNCS,...

    work page doi:10.1007/978-3-642-38171-3_11 2013

  55. [59]

    Majumdar, R., Sathiyanarayana, V.R.: Sound and Complete Proof Rules for Prob- abilistic Termination. Proc. ACM Program. Lang.9(POPL), 1871–1902 (2025). https://doi.org/10.1145/3704899

    work page doi:10.1145/3704899 1902

  56. [60]

    In: Steffen, B

    Matheja, C.: A Game-Based Semantics for the Probabilistic Intermediate Verifi- cation Language HeyVL. In: Steffen, B. (ed.) Bridging the Gap Between AI and Reality - Second International Conference, AISoLA 2024, Crete, Greece, October 30 - November 3, 2024, Proceedings. LNCS, vol. 15217, pp. 242–258. Springer, Heidelberg (2024).https://doi.org/10.1007/978...

    work page doi:10.1007/978-3-031-75434-0_17 2024

  57. [61]

    McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost- sure termination. Proc. ACM Program. Lang.2(POPL), 33:1–33:28 (2018).https: //doi.org/10.1145/3158121

    work page doi:10.1145/3158121 2018

  58. [62]

    Springer-Verlag, New York (2005)

    McIver, A., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer-Verlag, New York (2005)

    work page 2005

  59. [63]

    In: Groote, J.F., Larsen, K.G

    Meyer, F., Hark, M., Giesl, J.: Inferring Expected Runtimes of Probabilistic In- teger Programs Using Expected Sizes. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on The- ory and Practice of Software, ETAPS...

    work page doi:10.1007/978-3-030-72016-2_14 2021

  60. [64]

    In: Yoshida, N

    Moosbrugger, M., Bartocci, E., Katoen, J., Kov´ acs, L.: Automated Termination Analysis of Polynomial Probabilistic Programs. In: Yoshida, N. (ed.) Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg...

    work page doi:10.1007/978-3-030-72019-3_18 2021

  61. [65]

    In: Huisman, M., Pasareanu, C.S., Zhan, N

    Moosbrugger, M., Bartocci, E., Katoen, J., Kov´ acs, L.: The Probabilistic Termi- nation Tool Amber. In: Huisman, M., Pasareanu, C.S., Zhan, N. (eds.) Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20- 26, 2021, Proceedings. LNCS, vol. 13047, pp. 667–675. Springer, Heidelberg (2021). https://doi.org/10.1007/978-3-030-90870-6_36

    work page doi:10.1007/978-3-030-90870-6_36 2021

  62. [66]

    Moosbrugger, M., Stankovic, M., Bartocci, E., Kov´ acs, L.: This is the moment for probabilistic loops. Proc. ACM Program. Lang.6(OOPSLA2), 1497–1525 (2022). https://doi.org/10.1145/3563341

    work page doi:10.1145/3563341 2022

  63. [68]

    In: Proceedings of the 39th ACM SIGPLAN Con- ference on Programming Language Design and Implementation

    Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded Expectations: Resource Anal- ysis for Probabilistic Programs. In: Proceedings of the 39th ACM SIGPLAN Con- ference on Programming Language Design and Implementation. PLDI 2018. Asso- ciation for Computing Machinery, New York, NY, USA (2018).https://doi.org/ 10.1145/3192366.3192394 Caesar19

    work page doi:10.1145/3192366.3192394 2018

  64. [69]

    Springer (2002)

    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer (2002)

    work page 2002

  65. [70]

    ACM Trans

    Olmedo, F., Gretz, F., Jansen, N., Kaminski, B.L., Katoen, J., McIver, A.: Con- ditioning in Probabilistic Programming. ACM Trans. Program. Lang. Syst.40(1), 4:1–4:50 (2018).https://doi.org/10.1145/3156018

    work page doi:10.1145/3156018 2018

  66. [71]

    Machine Intelli- gence5(1969)

    Park, D.: Fixpoint Induction and Proofs of Program Properties. Machine Intelli- gence5(1969)

    work page 1969

  67. [72]

    MA thesis, RWTH Aachen University, Aachen (2024).https : / / doi

    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

    work page 2024

  68. [73]

    (2026).https://doi.org/10.5281/zenodo.19838026

    Schr¨ oer, P., Batz, K., Dural, U.Y., Haase, D., Kaminski, B.L., Katoen, J.-P., Math- eja, C.: Caesar: A Deductive Verifier for Probabilistic Programs (CAV26 Artifact), Zenodo. (2026).https://doi.org/10.5281/zenodo.19838026

    work page doi:10.5281/zenodo.19838026 2026

  69. [74]

    Schr¨ oer, P., Batz, K., Kaminski, B.L., Katoen, J., Matheja, C.: A Deductive Ver- ification Infrastructure for Probabilistic Programs. Proc. ACM Program. Lang. 7(OOPSLA2), 2052–2082 (2023).https://doi.org/10.1145/3622870

    work page doi:10.1145/3622870 2052

  70. [75]

    In: Computer Vision – ECCV 2018

    Schr¨ oer, P., Haase, D., Katoen, J.: Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing. In: Krebbers, R. (ed.) Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy,...

    work page doi:10.1007/978- 2026

  71. [76]

    In: Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18–22, 2026, Proceedings

    Schr¨ oer, P., Katoen, J.: Highly Incremental: A Simple Programmatic Approach for Many Objectives. In: Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18–22, 2026, Proceedings. LNCS, Springer, Heidelberg (2026)

    work page 2026

  72. [77]

    (2024).https: / / github

    Tristan, J.-B.: SampCert : Verified Differential Privacy, version 1.0.0. (2024).https: / / github . com / leanprover / SampCert.https : / / doi . org / 10 . 5281 / zenodo . 11204806

    work page 2024

  73. [78]

    Zaiser, F., Murawski, A.S., Ong, C.L.: Guaranteed Bounds on Posterior Distribu- tions of Discrete Probabilistic Programs with Loops. Proc. ACM Program. Lang. 9(POPL), 1104–1135 (2025).https://doi.org/10.1145/3704874

    work page doi:10.1145/3704874 2025

  74. [79]

    (2023).https://github.com/dafny-lang/Dafny-VMC

    Zetzsche, S., Tristan, J.-B.: Dafny-VMC: a Library for Verified Monte Carlo Algo- rithms, Software. (2023).https://github.com/dafny-lang/Dafny-VMC

    work page 2023