6 posts tagged with "publications"

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.