We present Caesar, a verifier for probabilistic programs. It was first published as part of a new deductive verification infrastructure for probabilistic programs at OOPSLA ’2023. In the following, we provide a condensed version that focuses on the basics of the verification infrastructure and the implementation Caesar.

The infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (IVL) together with a real-valued logic. The IVL provides a programming-language-style for expressing verification conditions whose validity implies the correctness of a program under investigation. As the focus is on verifying quantitative properties such as bounds on expected outcomes, expected run-times, or termination probabilities, off-the-shelf IVLs based on Boolean first-order logic do not suffice. Instead, a paradigm shift from the standard Boolean to a real-valued domain is required.

The IVL features quantitative generalizations of standard verification constructs such as assume and assert statements. Verification conditions are generated by a semantics in the weakest-precondition-style, using the real-valued logic. With the SMT-based implementation, a variety of benchmarks is automatically verified. To the best of our knowledge, this established the first deductive verification infrastructure for expectation-based reasoning about probabilistic programs.