The tool paper “Caesar: A Deductive Verifier for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Umut Yiğit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja has been accepted for presentation at the 38th International Conference on Computer Aided Verification (CAV 2026), to be held in Lisbon, Portugal.

The paper reports on five years of development of Caesar, a deductive verifier for probabilistic programs. Compared to the earlier OOPSLA 2023 paper on HeyVL and HeyLo, this tool paper focuses on Caesar as a practical verification tool. It presents the SMT-based pipeline via Z3 together with several newer features, including the Caesar Verifier VSCode extension, support for limited functions and improved quantifier handling, the JANI/Storm model-checking backend, stronger soundness checks and semantic guardrails for proof-rule usage, and slicing-based diagnostics.

More information is available on the Caesar website and in our Caesar blog post about the paper.