Caesar: A Deductive Verifier for Probabilistic Programs

TL;DR

Caesar is a deductive verifier for probabilistic programs that uses a new intermediate language HeyVL and integrates SMT solving with probabilistic model checking.

Contribution

It introduces HeyVL, a flexible intermediate language for probabilistic verification, and combines deductive and model-checking approaches in Caesar.

Findings

Supports proof rule extension and improved diagnostics.

Includes a probabilistic model checking backend.

Has been developed over five years with ongoing enhancements.

Abstract

Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL allows users to express a probabilistic program, its specifications, and proof rules in a programming-language style, so that new proof rules can be easily integrated into the verifier. Caesar translates HeyVL programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes a backend based on probabilistic model checking for a subset of HeyVL. We report on the results of five years of development of Caesar, highlighting its main features and architecture. In particular, we describe recent improvements such as additional proof rules, a model-checking backend, and better diagnostics.