One post tagged with "releases"

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.