6 posts tagged with "releases"

Caesar 4.1 fixes soundness bugs in @ast, @past, and @omega_invariant that could let invalid proofs pass verification. It also introduces @uwlp, extends @ast to finite demonic nondeterminism, infers loop terminators, and adds HeyVL reference hovers in Visual Studio Code.

Overview:

1. Almost-Sure Termination: @ast
2. Positive Almost-Sure Termination: @past
3. ω-Invariants: @omega_invariant
4. Unbounded Liberal Pre-expectations: @uwlp
5. Simpler Loop Unrolling
6. Visual Studio Code
7. Other Fixes

Caesar 4.0 improves expression parsing, adds explicit soundness guarantees for refutations in CLI/LSP feedback, introduces new weigh and additive choice (if +) statements, and experimental entailment checking.

Overview:

1. Expression Parsing Changes
2. Soundness Checks and Better Diagnostics
3. New HeyVL Statements: weigh and Additive Choice
4. Experimental Entailment Checking
5. Other Improvements

Caesar 3.0 improves the SMT reasoning capabilities of Caesar, making verification more powerful, stable, and predictable. This release marks the conclusion of a project that started more than 9 months ago, including a successful Master's thesis by Emil-Beothy Elo.

Overview:

1. Limited Functions
2. Other SMT-related Improvements
3. Other Improvements

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

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

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