Tool Paper on Caesar Accepted at CAV 2026
Our tool paper "Caesar: A Deductive Verifier for Probabilistic Programs" was accepted as a tool paper at CAV 2026, to be held in Lisbon, Portugal. The authors are Philipp Schröer, Kevin Batz, Umut Yiğit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja.
The paper reports on five years of Caesar development and presents Caesar as a deductive verifier for probabilistic programs in its current form: from the HeyVL/HeyLo core and the SMT-based pipeline via Z3 to the surrounding tooling and verification features. Compared to our earlier OOPSLA 2023 paper, which introduced the formal foundations of HeyVL and HeyLo, the new tool paper focuses on Caesar as a practical verification tool. Among the additions highlighted in the paper are the Caesar Verifier VSCode extension, support for limited functions and improved quantifier handling, the model checking backend via JANI and Storm, stronger soundness checks and guardrails for proof-rule usage, and slicing-based diagnostics.
The paper builds on our earlier OOPSLA paper "A Deductive Verification Infrastructure for Probabilistic Programs" (announcement post). In particular, it covers:
- the Caesar Verifier VSCode extension, which is now the recommended way to use Caesar;
- support for limited functions and improved quantifier handling;
- the model checking backend via JANI and Storm;
- stronger soundness checks for proof rules and additional guardrails for sound verification, building on Caesar's calculus annotations and the "More Guardrails" release;
- slicing-based diagnostics and related user-facing tooling.
If you want to explore these features on this website, the most relevant documentation is: