Skip to main content

About Caesar

Caesar is a deductive verification infrastructure specifically designed for probabilistic programs. That means it is a tool to provide formal guarantees for programs that incorporate probabilistic behaviours, such as drawing random numbers or making random choices.

Probabilistic programs can be found in randomized algorithms, communication protocols, machine learning models, and many other domains. When designing or analyzing such programs, many questions can be formulated with respect to some kind of expected value, such as the probability of reaching a certain state, the expected number of steps until a certain event occurs, or the expected value of some variable at the end of the program. We support the use of different proof rules, from areas such as martingale analysis or domain theory, thus enabling reasoning about programs with infinite state spaces and unbounded loops.

Caesar aims to be a verification infrastructure that combines many different techniques to formally reason about such expected values. We want to provide a tool that automates the verification process as much as possible, while still allowing the user to guide the verification process and provide additional information when needed. This differs from probabilistic model checkers such as Storm or PRISM, which are more "push-button" approaches that require less user interaction but struggle with e.g. infinite state spaces.

Caesar is an open-source project from RWTH Aachen University (MOVES group), Saarland University (QUAVE group), Denmark Technical University (SSE section), and University College London (PPLV group). The source code is available on GitHub. The name "Caesar" comes from "veni, vidi, vc", where we let "vc" stand for "verification conditions".

Main Features

  • Verification of expected values in probabilistic programs
  • Support for infinite state spaces, unbounded loops, and recursion
  • Support for different proof rules, such as from martingale analysis or domain theory
  • Integration with SMT solvers and probabilistic model checkers
  • Program slicing for error localization and hints
  • Integration with Visual Studio Code

Key Components

The Quantitative Intermediate Verification Language HeyVL

The architecture of Caesar is inspired by modern program verifiers that use an intermediate verification language (IVL) to encode a program, its specification, and proof rules into a common representation. Our quantitative IVL is called HeyVL. HeyVL generalizes classical IVLs to the quantitative setting through HeyLo, our new quantitative logic developed for Caesar. The names come from Heyting algebras, which underlie the logic.

In Caesar, HeyVL also has high-level constructs such as loops or procedure calls, but these are all encoded into a smaller core language. This core language and many encodings are described in our OOPSLA 2023 publication "A Deductive Verification Infrastructure for Probabilistic Programs".

Backends: SMT Solving and Probabilistic Model Checking

Caesar uses the Z3 SMT solver to reason about HeyVL programs. This allows Caesar to use symbolic reasoning to prove properties of probabilistic programs, enabling reasoning about infinite state spaces and unbounded loops. It is also possible to use other SMT solvers (by emitting SMT-LIB).

In addition, Caesar has a model checking backend that emits files in the JANI format, a JSON-based interchange format for probabilistic models. This is possible for an "executable" subset of HeyVL programs that can be translated into JANI models. The result can be fed into probabilistic model checkers such as Storm.

Slicing for Error Localization and Hints

Caesar includes a program slicing engine called Brutus (get it?) that reduces HeyVL programs with respect to certain properties. Slicing is Caesar's theoretical and practical foundation for error localization and hints. For example, by removing assertions from the program, we can find out the remaining assertions which must cause a verification failure.

Visual Studio Code Integration

We value usability and user-friendliness highly and want to make Caesar as easy to use as possible. It is our belief that UX is a key factor in making formal verification succeed in practice. This is why we put a lot of effort into integrating Caesar with Visual Studio Code with our Caesar for VSCode extension.

Disclaimer: (Un)Related Work

Caesar should not be confused with the set of tools in the CADP toolbox by INRIA, which includes tools like the CAESAR or CAESAR.ADT compilers, or the OPEN/CAESAR software architecture.