Skip to main content

Academic Publications

Caesar is a project from a collaboration of the Chair for Software Modeling and Verification (MOVES) at RWTH Aachen University, the QUAVE group at Saarland University, the PPLV group at University College London and the SSE section at Denmark Technical University.

If you are interested in collaborations or simply have some questions, please reach out to Philipp Schroer (phisch@cs.rwth-aachen.de).

Citing Caesar

For publications about Caesar, please cite our OOPSLA '23 paper (BibTeX file):

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs. Proceedings of the ACM on Programming Languages 7, OOPSLA 2023. DOI: https://doi.org/10.1145/3622870.

Overview:

Peer-Reviewed Papers​

OOPSLA '25: Foundations for Deductive Verification of Continuous Probabilistic Programs​

The paper "Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back" by Kevin Batz, Joost-Pieter Katoen, Francesca Randone, and Tobias Winkler was recently published at OOPSLA 2025. DOI: https://doi.org/10.1145/3720429.

This paper lays out the formal foundations for us to verify probabilistic programs that sample from continuous distributions, with support for loops, and conditioning. One challenge is to integrate the integrals for the expected values that arise from continuous distributions into the deductive verification framework of Caesar. The key idea is to soundly under- or over-approximate these integrals via Riemann sums. In addition to theoretical results such as convergence and completeness of the approach, the paper also provides case studies of continuous probabilistic programs that are encoded in HeyVL and verified with Caesar.

See our blog post for more details and examples.

AISoLA '24: A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL​

The publication "A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL" by Christoph Matheja was published at AISoLA 2024. DOI: https://doi.org/10.1007/978-3-031-75434-0_17.

Quoting from its abstract:

[T]he original language [HeyVL] lacked a formal “ground truth” in terms of a small-step operational semantics that enables an intuitive reading of HeyVL programs.

In this paper, we define an operational semantics for a cleaned-up version of HeyVL in terms of refereed stochastic games, a novel extension of simple stochastic games in which a referee may perform quantitative reasoning about the expected outcome of sub-games and give one player an advantage if those sub-game are outside of certain boundaries.

This new operational semantics is aimed at improved intuition and ergonomics of HeyVL, as well as a possible future work enabling other verification backends such as ones based on probabilistic model checking tools.

OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs​

HeyVL and Caesar were first published at OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs by Schröer et al. This paper introduces HeyLo and HeyVL with formal semantics, and explains how different proof rule encodings work.

For publication, please cite as follows (BibTeX file):

Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs. Proceedings of the ACM on Programming Languages 7, OOPSLA 2023. DOI: https://doi.org/10.1145/3622870.

An extended version with proofs, details on encodings, and typo fixes is available on arXiv: A Deductive Verification Infrastructure for Probabilistic Programs (extended version) — arXiv:2309.07781.

The artifact for our OOPSLA '23 publication is available on Zenodo. It has received the Distinguished Artifact award, praising exceptionally high quality of the artifact.

A video of the OOPSLA '23 presentation is available on YouTube:



We also presented this paper at the Dafny 2024 workshop, see the video below:

Bachelor and Master Theses​

Below are some selected theses that contributed to the development of Caesar and HeyVL.

Master Thesis '25: Effective Quantifier-based Reasoning for Quantitative Deductive Verification​

"Effective quantifier-based reasoning for quantitative deductive verification" is a Master thesis written by Emil Beothy-Elo at RWTH Aachen University. This thesis investigates different encodings of user-defined recursive functions as limited functions to avoid matching loops in the context of Caesar. It provides formal definitions and soundness proofs for several encodings used by other verifiers, and examines how one of the encodings can be modified to obtain finite and constructible counterexamples involving recursive functions. The results of this thesis have been implemented in Caesar (as of Caesar 3.0.0).

The PDF file is available online.

Abstract

Caesar is a deductive verifier for probabilistic programs. It builds on modern SMT solvers to automatically check if probabilistic programs conform to their specification. This high degree of automation sometimes comes at the cost of brittle verification. Seemingly unrelated changes in the input program can cause the verifier to hang and verification to fail. These instabilities are often caused by quantifiers that are used in axioms to describe the relevant theories for verification. A common problem here are matching loops - an ill-behaved set of quantifiers that can cause an infinite number of quantifier instantiations by themselves. A large contributor of matching loops are user-defined recursive functions. A common approach taken by other verifiers is to encode such functions as limited functions, limiting the number of recursive instantiations and avoiding matching loops by construction. While they have been proven to be effective, there is little information available about them and they lacked a formal treatment. We present and formally define different limited function encodings used by other verifiers, and subsequently prove that these transformations are sound. Furthermore, we examine how one of the encodings can be modified to obtain finite and constructible counterexamples involving recursive functions. The presented encodings are implemented in Caesar. We provide guidance on the subtleties that are required for the encodings to work well in practice. Our evaluation shows that the implemented encodings are very effective in eliminating brittleness for problematic programs in Caesar's test suite.

Master Thesis '25: Practical Probabilistic Program Verification using Caesar​

"Practical Probabilistic Program Verification using Caesar" is a Master thesis by Franka van Jaarsveld written at the University of Twente. It uses the Bounded Retransmission Protocol (BRP) as a case study to explore the practical verification of probabilistic programs using Caesar and gives insights into the strengths and limitations of Caesar in practice.

The PDF file is available via the UT Student Theses website.

Abstract

This thesis explores the practical verification of probabilistic programs using Caesar, a weakest preexpectation-based verification tool for reasoning about the expected behaviour of discrete probabilistic programs. The Bounded Retransmission Protocol (BRP) is studied as a case study. A key contribution of this work is the abstraction and decomposition of BRP into two geometric-like programs, enabling more effective reasoning about the protocol's behaviour and facilitating the stepwise verification strategy. Theoretical verification of key properties (positive almost-sure termination, success probability, and the expectation of the number of failed and sent transmissions) was largely successful using weakest preexpectation calculus. Translating these results into verification using Caesar introduced practical challenges, particularly in invariant discovery. Additionally, even valid invariants did not always lead to successful verification due to limitations in Caesar’s current implementation, particularly in SMT solver performance and the handling of exponentials. However, through workarounds including alternative invariants and a 'fueled' exponential function, meaningful properties of BRP were verified. This thesis demonstrates how such techniques support practical verification in Caesar and concludes with a discussion of its strengths, limitations, and recommendations for effective use.

Master Thesis '22: A Deductive Verifier for Probabilistic Programs​

Caesar is based on a 2022 Master thesis by Philipp Schroer entitled "A Deductive Verifier for Probabilistic Programs". This thesis contains the foundations for Caesar, HeyVL, and HeyLo, including encodings for Park induction, k-induction, and bounded model checking. It also discusses the implementation of Caesar with its prenexing-based quantifier elimination and presents early experimental results.

The PDF file is available online.

Abstract

We design and implement a deductive verification infrastructure for probabilistic programs. It consists of a quantitative intermediate verification language (HeyVL) and a quantitative assertion language (HeyLo). HeyLo is a syntax to express expected values of probabilistic programs, with support for quantitative implications based on Gödel logic. Both HeyLo and HeyVL contain lattice-theoretic dual constructs to reason about lower and upper bounds of expected values. As a case study, we encode weakest pre-expectation and weakest liberal pre-expectation reasoning about the probabilistic programming language pGCL into HeyVL. For loops, we provide encodings of Park induction, k-induction, and bounded model checking. Park induction and k-induction are both proof rules that require on user-provided invariant candidates. Furthermore, we discuss the automation of our deductive verification infrastructure. Our implementation Caesar takes a HeyVL program as input, generates and optimizes verification conditions in the form of HeyLo formulas and uses the automated theorem prover Z3 to prove or disprove validity of the verification conditions. In this thesis, we focus on the central optimization of quantifier elimination of HeyLo formulas. We present early promising experimental results. Finally, we discuss the abstraction of our framework based on Heyting and Gödel algebras to support more domains than expectations.

Compared to the OOPSLA '23 paper:

  • The thesis includes a large section on quantifier elimination (by prenexing) for the logic, which is omitted in the paper for brevity.
  • The thesis provides a more exploratory view on the logic, with e.g. a "relational view" on the semantics.
  • The thesis still uses negation statements, whereas the paper switches to validate statements to encode comparisons.
    • validate statements have monotonic semantics (in contrast to negation statements), which is easier to work with in general.

Citations:

For more background on the weakest pre-expectation-based approach to reasoning about probabilistic programs, we recommend the following publications:

Caesar uses SMT solvers as backends. For more information on SMT solving, we recommend: