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 Caesar 2.1 release adds contains various improvements to existing features and fixes some bugs.

Overview:

1. UI and Documentation Improvements
2. More Guardrails
3. Slicing Improvements
4. Minor Fixes

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.

We are happy to announce Caesar 2.0: the next release of Caesar packed with a lot of new features.

Overview:

1. Caesar Verifier Visual Studio Code Extension
2. Slicing for Error Reporting and Correctness
3. Calculus Annotations for Proof Rules
4. Model Checking Support via JANI

We are happy to announce that RWTH's MOVES group, headed by Prof. Joost-Pieter Katoen, will receive funding from the European Research Council (ERC) for a Proof of Concept Grant to improve Caesar.

On January 14, 2024, I presented Caesar and the basics of our quantitative intermediate language HeyVL at the Dafny 2024 workshop. The workshop was part of the POPL 2024 conference.

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.

Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, see here.