We are happy to announce Caesar 2.0: the next release of Caesar packed with a lot of new features.

Overview:

1. Caesar Verifier Visual Studio Code Extension
2. Slicing for Error Reporting and Correctness
3. Calculus Annotations for Proof Rules
4. Model Checking Support via JANI

Caesar Verifier Visual Studio Code Extension​

Our new Caesar Verifier VSCode extension is now the recommended way to use Caesar. The extension is available in the VSCode and VSCodium extension marketplaces and can be installed by searching for Caesar Verifier.

The extension is built on the Language Server Protocol and uses the Caesar binary under the hood.

Features:

• Syntax highlighting and language configuration for HeyVL.
• Snippets for HeyVL.
• Verify HeyVL files on file save or on command.
• Verification errors and successes are shown in the gutter via icons.
• Diagnostics such as errors or warnings are shown in the code and in the "Problems" menu in VSCode — powered by slicing!
• Inline explanations of computed verification conditions (shown in picture!).
• Automatic installation and updating of Caesar.

Slicing for Error Reporting and Correctness​

Assertion Slicing​

The error reports in Caesar are driven by the first implementation of specification-based slicing for probabilistic programs. By default, our slicing implementation is used to identify which assert-like statements are responsible for errors (Caesar's assertion slicing).

An example is shown on the right. The slicing algorithm has determined that the invariant might not be inductive and could rule out e.g. that the pre does not entail the invariant.

Caesar's slicing does not operate on high-level programs with loops, but instead on the low-level HeyVL statements, including verification statements. This enables error reporting (and other slicing applications) for any verification problems that you can encode in HeyVL. Custom error messages can be added via slice message annotations.

Assumption Slicing​

Whereas assertion slicing is concerned with finding a minimal set of assertions in the program so that the program still has an error, assumption slicing tries to find a minimal set of assumptions so that the program still verifies.

In the example on the right, we can see a slightly modified version of the geometric loop example from above. Now it has a constant starting value of zero. With the correct invariant, the program verifies. But Caesar can also tell us that this while loop could also be an if statement — no loop is required to satisfy the specification. The interpretation of this result is up to the user. Maybe the program can be simplified, but maybe the specification is not as strong as one thought and needs to be strengthened!

General Slicing​

Caesar's implementation of slicing is not restricted to verification statements such as assertions and assumptions. With program annotations, Caesar can be instructed to run slicing for correctness and try to eliminate unnecessary assignments from the program.

In the example on the right, we have a probabilistic program that encodes a Bayesian network.¹ We have added the @slice_verify annotation to have Caesar also try to slice assignments. Caesar determined that most assignments are not necessary to satisfy the specification.

There is also a corresponding @slice_error annotation to do slicing for errors on statements that are not assert-like.

Calculus Annotations for Proof Rules​

Caesar's HeyVL was designed as a quantitative intermediate verification language, therefore it allows encoding all sorts of potentially unsound proof rules. To make it easier to use Caesar to verify high-level programs with loops with respect to well-known expectation-based calculi and proof rules, we have added calculus annotations to Caesar. They are @wp, @wlp and @ert. When they are added to a proc/coproc, Caesar will do some additional checks to ensure that proof rules are actually sound.

Model Checking Support via JANI​

While deductive verification can deal with infinite state spaces, infinite data types, and is generally pretty awesome, sometimes you want to analyze a proabilistic program whose state space can be finitely represented. With Caesar's model checking support via JANI, you can export your probabilistic program to the JANI format to use probabilistic model checkers.

Caesar's support is limited to executable probabilistic programs. That means that quantitative verification statements like assert, assume, and havoc are restricted or not supported.

Caesar's JANI export was designed as a replacement for the recently deleted storm-pgcl, and can now be used as a pGCL frontend for model checkers that accept JANI inputs.

We are happy to announce that RWTH's MOVES group, headed by Prof. Joost-Pieter Katoen, will receive funding from the European Research Council (ERC) for a Proof of Concept Grant to improve Caesar.

Caesar was originally built in part through FRAPPANT, the 2018 ERC Advanced Grant "Formal Reasoning about Probabilistic Programs: Breaking New Ground for Automation". The new ERC Proof of Concept research proposal "A Deductive Verifier for Probabilistic Programs (VERIPROB)" is about applying knowledge from FRAPPANT to build Caesar into a prototype that can be made use of by industry — "to turn science into practice".

See also the press release by the university and the ERC announcement.

On January 14, 2024, I presented Caesar and the basics of our quantitative intermediate language HeyVL at the Dafny 2024 workshop. The workshop was part of the POPL 2024 conference.

The talk starts at timestamp 7:16:23 and ends at timestamp 7:34:00.

The artifact associated with our OOPSLA '23 publication A Deductive Verification Infrastructure for Probabilistic Programs has received the Distinguished Artifact award, praising exceptionally high quality. The artifact consists the tool Caesar together with benchmark examples.

The artifact has a page in the ACM Digital Library and can be downloaded from Zenodo.

HeyVL and Caesar were accepted at OOPSLA '23: A Deductive Verification Infrastructure for Probabilistic Programs by Schröer et al. The artifact received the reusable badge, which is the highest possible badge.

The preprint is available on arxiv: https://arxiv.org/abs/2309.07781.

You can find more information on our publications page.

Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, see here.