Skip to content

Version 4.5.0
Compare
Choose a tag to compare
@smitsch smitsch released this 09 Jul 20:13
· 5817 commits to master since this release
4.5.0
This tag was signed with the committer’s verified signature.
LSLabBuild
GPG key ID: 9C461005FDEDB15E
Learn about vigilant mode.
94bfbdb

Version 4.5.0 provides a major update to the invariant generation and proving techniques for differential equations in its automated ODE tactic.

  • [New] Pegasus invariant generator for differential equations

  • [New] ODE automation tactics for axiomatic proofs from differential ghost and differential refinement axioms, proofs of barrier certificates, and proofs of invariance properties that involve Darboux polynomials

  • [Preview] Invariant generation for loops based on fixpoint-search over invariants for differential equations

  • [Tactics] Liveness: loop convergence with user-definable convergence variable, improved <:=> assignment tactics

  • [Tactics] Extended proof search automation in the context of universal/existential quantifiers

  • [Tools] C code generator for structured monitors with sub-routines and error message printing

Assets 3