7 posts tagged with "publications"

Our new paper "Highly Incremental: A Simple Programmatic Approach for Many Objectives" by Philipp Schröer and Joost-Pieter Katoen presents a one-fits-all approach for quantitative objectives on probabilistic programs, applicable to verification with Caesar.

The paper will be presented at The 27th International Symposium on Formal Methods (FM 2026) in Tokyo, Japan.

A preprint with a detailed appendix of proofs and case studies is available on arXiv: "Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)".

In this post, we:

1. show how reward statements model runtime and related quantities.
2. explain why verification of variance is difficult for runtime objectives.
3. introduce our sound program transformation for these objectives, including higher moments, tail probabilities, CDFs, expected excess, and moment-generating functions.
4. work through a Caesar example for the second moment of runtime.

Programmatic Reward Modeling​

The paper explores what can be encoded into probabilistic programs with reward statements, which collect a certain quantity — rewards — during execution. We then consider expected rewards, i.e. the expected value of rewards collected over the distribution of program executions. This approach enables more applications for Caesar's weakest pre-expectation reasoning out-of-the-box.

The paper "Verifying Almost-Sure Termination for Randomized Distributed Algorithms" was presented at the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL) 2026 held in Rennes, France. The authors are Constantin Enea (LIX, CNRS, Ecole Polytechnique), Rupak Majumdar (MPI-SWS), Harshit Jitendra Motwani (MPI-SWS), V.R. Sathiyanarayana (MPI-SWS).

The paper presents a verification technique for liveness properties of randomized distributed algorithms. It introduces a proof rule for fair almost-sure termination of distributed systems, combining martingale-based arguments for probabilistic termination with reasoning about weak fairness. The proof rules are implemented in Caesar and were used to verify termination of randomized asynchronous consensus protocols, including Ben-Or’s protocol and graded binary consensus, under both crash and Byzantine faults.

Our paper "Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing" was accepted at the European Symposium on Programming (ESOP) 2026 to be held in Turin, Italy. The authors are Philipp Schröer, Darion Haase, and Joost-Pieter Katoen. An extended version of the paper is already available on arXiv.

The paper presents theoretical foundations and the implementation of our slicing-based user diagnostics in Caesar, which we dub Brutus. On this website, you can also find the user guide-level documentation on slicing in Caesar. See also the announcement of Caesar 2.0, which introduced the first slicing implementation in Caesar.

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.

Before this work, Caesar was able to only verify simple discrete probabilistic programs, i.e. programs that only sample from discrete distributions. 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.

In this post:

1. Encoding Riemann Sums in HeyVL
2. Tortoise-Hare Race Example
3. Beyond The Continuous Uniform Distribution

The paper "A Game-Based Semantics for the Probabilistic Intermediate Verification Language HeyVL" by Christoph Matheja was published at AISoLA 2024 and is now available online.

The artifact associated with our OOPSLA '23 publication A Deductive Verification Infrastructure for Probabilistic Programs has received the Distinguished Artifact award, praising exceptionally high quality.

HeyVL and Caesar were accepted at OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs by Schröer et al. The artifact received the reusable badge, which is the highest possible badge.