Skip to main content

Caesar 2.1: UI Improvements, More Guardrails, and Improvements to Slicing

ยท 4 min read
Philipp Schroer
Philipp Schroer
Caesar Developer

The Caesar 2.1 release adds contains various improvements to existing features and fixes some bugs.

Overview:

  1. UI and Documentation Improvements
  2. More Guardrails
  3. Slicing Improvements
  4. Minor Fixes

UI and Documentation Improvementsโ€‹

We have improved Caesar's UI, especially the Visual Studio Code extension. Thanks to PRs #48 and #60:

  • We now properly support verification with multiple open HeyVL files (before, the extension only remembered the latest verification task). This includes error messages and warnings.
  • We improved the wording in the status bar to more accurately reflect the verification status.
  • Proper handling of "unknown" results from the SMT solver.
  • The tooltip menu on the status bar is much more dynamic and supports more features depending on verification results.

PR #59 added verification condition explanations for the @unroll proof rule.

Additionally:

  • We now automatically start the Caesar LSP server if a HeyVL file is opened.
  • The default timeout for Caesar in VS Code is now 60 seconds (previously it was 300 seconds).
  • The documentation for various features of Caesar has been improved with notes about some relevant theoretical aspects.

More Guardrailsโ€‹

Caesar now prevents accidental unsound verification through more "guardrails". This extends the soundness checks from calculus annotations feature introduced in the last release. Thanks to PR #42:

  • We now check that procedures only call other procedures with the same calculus annotations.
    • If either the caller or callee has no calculus annotation, we do not currently warn the user.
  • We now check that procs are only called inside procs (and analogously for coprocs).
  • Various other checks for proof rule annotations have been improved.

Improvements to Slicingโ€‹

We have been hard at work to complete and further improve Caesar's slicing support.

  • We now support slicing probabilistic choices via the command-line flag --slice-sampling.
    • This is disabled by default because we have observed negative performance effects for relatively little gain in the average case.
  • Caesar now uses irrelevancy information from the SMT solver to speed up the slice search.
  • Caesar no longer highlights the entire procedure if it does not have a pre when slicing for verification.
  • We now properly slice demonic and angelic choices.

We added additional slicing backends to slice verifying programs:

  • A slicing backend on unsatisfiable cores was added (core). It is very fast, but does not report optimal slices in many cases.
    • This backend is now the default when slicing verifying programs.
  • We implemented minimal unsat core enumeration to support finding the locally or globally smallest slices (mus and sus backends).
  • The old exists-forall backend still exists, but is not recommended for the general use case because it does not support reasoning with uninterpreted functions.

Command-Line Interfaceโ€‹

Caesar's command-line interface has been redesigned. The binary now accepts different sub-commands to enable different tasks.

  • The new verify command includes all behavior of the previous Caesar CLI interface.
    • If no sub-command is specified, this command will be used. Therefore, the command-line interface is backwards-compatible.
  • The to-jani command can be used to only convert HeyVL files to JANI files without running Caesar's checks or verification.
  • The shell-completions command can be used to generate code for shell completions for the caesar binary.

Furthermore:

  • Caesar's --help output is now much more organized and helpful.
  • A new --no-verify option can be used to skip the final SMT check. This is useful in conjunction with either --print-smt or --smt-dir options.
  • The --print-smt and --smt-dir flags will now emit the SMT-LIB code before the final SMT call happens to avoid no output on timeouts.

Minor Fixesโ€‹

We have also fixed minor issues, for example:

  • Proper error reporting when using the @k_induction proof rule with the invalid parameter k = 0.
  • The --smt-dir flag now works properly on Windows.
  • Fixed syntax highlighting of block comments in VS Code.