Skip to main content

4 posts tagged with "publications"

View All Tags

Foundations for Verification of Continuous Programs with Caesar

· 4 min read
Philipp Schroer
Caesar Developer

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