Skip to main content

Caesar 2.2: Timeout Handling, Recursion Checks, Improved Model Checking, and More

· 3 min read
Philipp Schroer
Philipp Schroer
Caesar Developer

The Caesar 2.2 is an incremental release that adds various improvements to existing features and fixes some bugs.

Overview:

  1. UI Improvements
  2. Guardrail Against Unsound Recursion
  3. Better Model Checking Support
  4. AST Rule Improvements
  5. Other Changes

UI Improvements​

We have improved Caesar's LSP server and the Visual Studio Code extension.

  • The extension now properly handles Caesar timeouts.
  • Gutter icons are now shown for more verification statuses (todo, ongoing, timeout).

On the command-line:

  • Caesar now supports the --filter [<filter>] command-line argument to filter the (co)procs that are to be verified or translated for model checking.

Guardrail Against Unsound Recursion​

We have added a new check to prevent unsound recursion in the calculus annotations feature. This check ensures that users do not accidentally invoke Park induction in an unsound way in the presence of recursive (co)procedures. It is based on a call graph analysis of the program and over-approximates potential recursion.

Better Model Checking Support​

Caesar's support for model checking has been greatly improved in this release. First of all, it gained a new subcommand caesar mc to run the model checker on a given HeyVL file.

Many bugs have been fixed and improvements have been made to the model checking support:

  • Correct extraction of preconditions from coprocs.
  • Support non-integer rewards.
  • Support for different behaviours of uninitialized variables in the translation has been added.
  • Support for translation of more verification statements (specific forms of assume, assert) has been added.
  • Only required function definitions are now included in the translation.
  • Caesar now supports directly invoking the Storm model checker via either an installed binary or by using a Docker image.
  • Input variables can be translated as variables or as constants now.

AST Rule Improvements​

We have updated the "New Proof Rule for AST" to be more general, allowing verification of AST for more programs. This is a result of a combination of different formulations in the literature, our own theoretical improvements, as well as internal code improvements for the implementation.

We have added new documentation for general AST proofs and for this specific AST proof rule in particular.

Other Changes​

  • Documentation has been improved in many places.
  • Caesar now supports Z3's probes to determine theoretical complexities of verification tasks.

Many internal improvements to the slicing algorithms have been made.

  • Improved robustness against Z3's incremental mode instabilities.
  • Fixed the sus algorithm not finding optimal slices with non-extensive statements.
  • Clarified minimality guarantees of the different algorithms.

Internal:

  • Caesar's test files have been updated to consistenly use the built-in proof rules instead using the old Python-generated HeyVL encodings.
  • Caesar has been updated to compile with latest versions of backwards-incompatible C++ compilers and new versions of CMake.