Caesar 2.1.0 release

Cargo.toml

@@ -7,7 +7,7 @@ members = [
 
 [package]
 name = "caesar"
-version = "2.0.8"
+version = "2.1.0"
 authors = ["Philipp Schroer <[email protected]>"]
 description = "Caesar is a deductive verifier for probabilistic programs."
 homepage = "https://www.caesarverifier.org/"

vscode-ext/package.json

@@ -3,7 +3,7 @@
   "displayName": "Caesar Verifier",
   "description": "The quantitative deductive verifier Caesar for VSCode",
   "publisher": "rwth-moves",
-  "version": "2.0.8",
+  "version": "2.1.0",
   "repository": {
     "type": "git",
     "url": "https://github.com/moves-rwth/caesar.git",

website/blog/2025-01-17-caesar-2-1.md

@@ -0,0 +1,91 @@
+---
+authors: phisch
+tags: [releases]
+---
+
+# Caesar 2.1: UI Improvements, More Guardrails, and Improvements to Slicing
+
+The *Caesar 2.1* release adds contains various improvements to existing features and fixes some bugs.
+
+**Overview:**
+
+ 1. [UI and Documentation Improvements](./2025-01-17-caesar-2-1.md#ui-and-docs)
+ 2. [More Guardrails](./2025-01-17-caesar-2-1.md#more-guardrails)
+ 3. [Slicing Improvements](./2025-01-17-caesar-2-1.md#improvements-to-slicing)
+ 4. [Minor Fixes](./2025-01-17-caesar-2-1.md#minor-fixes)
+
+<!-- truncate -->
+
+## UI and Documentation Improvements {#ui-and-docs}
+
+We have improved Caesar's UI, especially the Visual Studio Code extension.
+Thanks to PRs [#48](https://github.com/moves-rwth/caesar/pull/48) and [#60](https://github.com/moves-rwth/caesar/pull/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](https://github.com/moves-rwth/caesar/pull/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](/docs/proof-rules/calculi) feature introduced in the last release.
+Thanks to [PR #42](https://github.com/moves-rwth/caesar/pull/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 `proc`s are only called inside `proc`s (and analogously for `coproc`s).
+ * 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](/docs/caesar/slicing).
+
+ * 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.