Introduction

Hello and welcome! This is the user documentation for Caesar, a deductive verification framework for probabilistic programs.

Overview

After installing Caesar, continue with our getting started guide to learn the basics of HeyVL and Caesar.

The language is documented in the HeyVL language section. Built-in functions and types are documented in the standard library section.

In the Caesar section, we have documentation for the Caesar tool, its command-line interface and the VSCode extension, as well as for our slicing algorithm.

Our Theory Paper

We have an OOPSLA 2023 paper on Caesar and its theory: A Deductive Verification Infrastructure for Probabilistic Programs. You can find the preprint on arxiv. More information on the publications page.

Contact Us!

This is research software, so it's not bug-free and there may be missing documentation in places. Please open start a discussion in our forum, open an issue, or send an email to phisch@cs.rwth-aachen.de with questions or ideas.