Version 4.8.0

Version 4.8.0 provides a restructured and reviewed microkernel and extended kernel. Extended differential equation invariant generation, and more flexible user definitions, significant performance improvements.

• [Core] Restructured and reviewed microkernel and extended kernel
• [Core] Design-separation between trusted external QE tools and additional non-soundness-critical external tools
• [Core] Semantic uniform renaming of rules
• [Core] Derived several axioms as lemmas
• [UI] Expand function, predicate, and program definitions on demand, introduce new definitions in the proof (e.g., abstract loop invariant predicate J(x,y,z) instead of concrete x+y>=z formula) and expand on demand later
• [UI] Auto-login for single-user environments
• [Tactic] New useSolver tactic to switch backend solver mid-proof, e.g., useSolver("Mathematica") or useSolver("Z3")
• [Backend] Extended invariant generator Pegasus for differential equations (linear and non-linear systems, improved generation strategy)
• [Backend] New native Java BigDecimal tool for variable-free exact arithmetic evaluation
• [Parser] Unicode game symbols for demonic choice '∩' and demonic repetition '×'
• [Performance] QE result caching
• [Performance] Faster parsing and printing of provables and lemmas
• [Performance] Faster lemma storage/retrieval from database
• [Performance] Runtime contracts disabled by default, can be enabled with java -ea and disabled with java -da
• [Platform] Updated support for latest Java Virtual Machine and JDK versions