Introduction

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

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.

---

This is research software and we're still working on a nice user interface, documentation, and fixing bugs. Do not hesitate to open an issue or send an email to phisch@cs.rwth-aachen.de with questions or ideas. I am also happy to discuss anything via Zoom as well!

---

Start with the quick start guide!

General things about the tool is documented in the Caesar chapter. We have a section on the pGCL frontend. There is also a chapter on the HeyVL language and the standard library.