What's new in KeYmaera 3.6.17
Mar 10, 2015
- Bugfix: Updated path for Mathematica 10.0.2, add support for Mathematica group license check
New in KeYmaera 3.6.16 (Mar 10, 2015)
- Bugfix: Undeclared variables in implementation of quantified differential invariants
New in KeYmaera 3.6.15 (Nov 15, 2014)
- Bugfix: Stable variable ordering in quantifier elimination, differential invariants with quantified variables
New in KeYmaera 3.6.14 (Nov 15, 2014)
- Bugfix: Mathematica license expiration check made on Mathematica 9
New in KeYmaera 3.6.13 (Nov 15, 2014)
- Add Khalil Ghorbal's implementation for differential radical invariants with conjunctions
New in KeYmaera 3.6.12 (Sep 5, 2014)
- Maintainance update, improve Mathematica interface
New in KeYmaera 3.6.11 (Sep 5, 2014)
- Minor update of user interface
New in KeYmaera 3.6 (Jul 25, 2014)
- Add barrier certificates and non-smooth barrier certificates by Andrew Sogokon
- Bugfix pretty printer for proof saving
- Bugfix parsers
- Add support for quantified differential invariants [24]
- Bugfix for Windows-specific user interface quirks
- Proofs store changes in decision procedures to remember collaborative decision procedure combinations
- Bugfix global taclets
- User interface fixes
New in KeYmaera 3.5 (Jul 25, 2014)
- Use theory-conform rules for nondeterministic choices, not derived rules
- Equality rewriting
- Global loop invariant handling
- Bugfix graphical user interface
New in KeYmaera 3.4 (Jul 25, 2014)
- New simulation engine for hybrid programs. Use Context menu->Plot Trajectory by Stefan Mitsch and Il Suk Lyu
- New KeYmaera Launcher wizard that makes it easy to install and run KeYmaera on your computer
New in KeYmaera 3.3 (Jul 25, 2014)
- Course 15-424/15-624 Foundations of Cyber-Physical Systems at CMU has KeYmaera-related lecture material
- Release Sphinx Verification-Driven Engineering Toolkit with textual and graphical modeling tools for KeYmaera
New in KeYmaera 3.2 (Jul 25, 2014)
- Built-in Min, Max functions
- Sqrt, Exp, Log, CubeRoot, E, Pi, Sin, Cos, Tan, Cot, Csc, Sec, ArcSin, ArcCos, ArcTan, ArcCot, ArcCsc, ArcSec
- Include robotic ground vehicle models and proofs [6]
- Proof strategies for extremely large proofs
New in KeYmaera 3.1 (Jul 25, 2014)
- Added support for MetiTarski solver and transcendental functions (Andrew Sogokon)
- Substantially improved support for implicit differential equations, which now no longer have to be written as differential-algebraic equations [38], but can remain implicit differential equations.
- Built-in support for functions like Abs for absolute value
- Look out for the course about Logics of Dynamical Systems at the EPCL European PhD Program in Computational Logic
- Look out for the upcoming summer school course about Logical Analysis of Hybrid Systems: The KeYmaera Approach at VSWSS
New in KeYmaera 3.0 (Jul 25, 2014)
- Kiki Proof Assistant teaches you how to use proof rules for complex systems. Enable Options->Proof Assistant
- Add new proof tactics
- New tutorial for KeYmaera at File->Start Tutorial, which is one resource for learning KeYmaera
- New KeYmaera Cheat Sheet
- Improve rule names and their explanations to fit to the theory [26,17]
- New and improved Project Wizard: use File->Load Project. Now supports direct links to authors and papers for projects listed in KeYmaera
- Add several neat studies to File->Load Project
- Implement new differential invariant generators [12]
- Implement (part of) the quantified differential dynamic logic (QdL) calculus for distributed hybrid systems [25,14] in KeYmaera
- Implement the differential dynamic game logic (dDGL) calculus for hybrid games [11]
- Add plotting for dynamical systems. After clicking on the differential equation modality select Plot Trajectory
- Add mechanism for abbreviations and conditional terms if-then-else
- Drag and drop hybrid programs for rule instantiations
- Implement differential auxiliaries [15]
- Add \programVariables block for declaring state variables, instead of having to declare variables as part of the hybrid program
- Special functions with built-in meaning like Sin, Cos, Pi, I can be declared via \external to avoid confusion with user-defined variables
- New strategy option determines how to handle differential equation solving
- Finally implement rich-test version of differential dynamic logic [39]
- Complete redesign of term transformation and solver interfaces
- Resolve built-in naming pitfalls of solver integration
- Improved automatic solver installation and configuration
- Add several neat examples to File->Load Project
- User interface improvements
New in KeYmaera 2.1 (Jul 25, 2014)
- KeYmaera 2.1 runs out of the box for many solvers
- Add automatic solver installation and configuration
- Built-in differential invariants and differential variants handling without external tool support
- Add support for solver-dependent proof loading
- Improve external solver integration
- Important bug fixes and stability improvements to prevent KeYmaera from occasionally stopping or becoming unresponsive when the interaction with external tools fails
- Numerous user interface improvements
- Look out for the upcoming tutorial about Logics of Dynamical Systems at LICS [17]
- Added support for Z3 SMT Solver by Microsoft Research
- Add new feature for improved counterexample transition finding contributed by Jingyi Ni.
- Improved proof strategies and proof automation
- A number of usability updates to KeYmaera 2.0
- Release KeYmaera Eclipse Plugin
New in KeYmaera 2.0 (Jul 25, 2014)
- New and more robust proof saving/loading
- Add View -> Mathematica Console
- Add more flexible and robust proof strategies
- New case studies in File->Load Project
- Be sure to checkout File->Load Project and then Load Proof for advanced proofs.
- Added several usability features and fixes that make it easier to use KeYmaera
- Look out for the tutorial about KeYmaera at FroCoS
- Updated features in KeYmaera release 1.9
- Add more case studies to Project Wizard
- Tell us if you want to include your KeYmaera case study.
- Tutorial about KeYmaera verification at CAV'11 [22]
New in KeYmaera 1.9 (Jul 25, 2014)
- New Feature: Uniform @annotation capabilities
- New Feature: Unicode formula notation
- New Features added to KeYmaera's Project Wizard
- Improved automation and proof strategy, including differential saturation, loop saturation, and (differential) invariant generation
- Add help browser to Project Wizard
- Add a lot more project examples to File->Load Project
- Improved and streamlined graphical user interface
- Rename proof rules consistently with book [26]
- New publication about verification of car control [23].
- New and improved KeYmaera Tutorial
- New and improved KeYmaera FAQ
- New publication introducing quantified differential invariants [25] for distributed hybrid systems.
- New publication introducing quantified differential dynamic logic (QdL) [25], which is the first formal verification approach for (dynamic/reconfigurable) distributed hybrid systems.
- Updated installers and windows support
New in KeYmaera 1.8 (Jul 25, 2014)
- New Feature: 2D mathematical formula notation and syntax highlighting
- New Feature: Simplified configuration management
- New Feature: Advanced arithmetic handling
- New Feature: Built-in quantifier elimination
- New Feature: More advanced projects (File->Load Project)
- New Feature: Java WebStart version contains all features
- An article introducing and developing the theory of differential invariants for verification in KeYmaera has appeared in print in Journal of Logic and Computation [38], as previously appeared in Advance Access on 12/18/2008.
- 1Best paper award of FM for a publication on formal verification of an aircraft maneuver in KeYmaera [29]
- Read about KeYmaera mentioned in the Brilliant 10 of 2009
- Read about this research in CMU News
- Read about KeYmaera research in Pittsburgh Post-Gazette
- Read about this research in CMU SCS News
- Publications on case studies in formal verification of hybrid systems in KeYmaera available [29,28]
- Announced NSF Expedition on CMACS
- Publication on advanced real arithmetic handling in KeYmaera has appeared at CADE [31]
- Background article on algorithmic computation of differential invariants has appeared in Formal Methods in System Design [32]. This is an algorithmic approach for the differential invariants introduced in [38]
- Started KeYmaera FAQ
New in KeYmaera 1.5 (Jul 25, 2014)
- New KeYmaera Installer with simplified setup
- Several improvements and bugfixes for the KeYmaera Webstart and KeYmaera Download
- Carnegie Mellon University press release regarding Cyber-Physical Systems Verification
- Major improvements in KeYmaera Webstart Version, which now supports Mathematica, Reduce/Redlog and QEPCAD B as optional solvers
- Simplified configuration management in KeYmaera
- Improved the KeYmaera Webstart Version
- Add while loop statement to hybrid programs
- Significant advances in automation and integration
- Built-in Gröbner Bases and Fourier-Motzkin elimination
- Interface with Redlog as a new optional background solver
- Improve integration of QEPCAD B as a background solver
- Interface with Gröbner Bases in built-in Orbital library
- Interface with CSDP as a background solver
- Several strategy and automation improvements
- Improved handling of real arithmetic
- New system specification language features
- Ph.D. thesis Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems
- Background article on extended logics behind KeYmaera introducing differential invariants has appeared in Journal of Logic and Computation advance access [38]
- Improved the KeYmaera Webstart Version with native QEPCAD support
New in KeYmaera 1.4.1 (Jul 25, 2014)
- KeYmaera now provides a brand new project assistant:
- click File->Load Project
- Interface QEPCAD B as a new background solver alternative for Mathematica
- Introduce differential inequality and differential inclusion handling [38]
- Add differential refinement support for differential constraints [38]
- Faster startup
- Background article on the logic and theory behind KeYmaera has appeared in Journal of Automated Reasoning [39]
- Slides on KeYmaera Tool Paper [33]
- KeYmaera tool paper appeared at IJCAR in LNCS [33]
- Publication on algorithmic computation of differential invariants appeared at CAV [35] based on the theory in [38]
- Improved the KeYmaera Webstart Version
- Better proof presentation and rendering
- Background article on the logic and theory behind KeYmaera to appear in Journal of Automated Reasoning [39]
- Equational Gröbner basis verification support
- Built-in arithmetical simplifier support
- Improved prover automation
- Released automatic invariant and differential invariant discovery procedure [35]
- KeYmaera supports differential invariants [38]
- Improved automated handling of existentially quantified properties [39]
- User interface improvements
- KeYmaera now supports proof @annotations.
- Improved and faster quantifier handling.
- Transition system views can be generated automatically, e.g., the ETCS transition system example.
- First public release of KeYmaera: Release KeYmaera 1.1
- Publication on proof procedures and deduction modulo theory in KeYmaera at VERIFY [40]
- Slides on differential dynamic logic [41]
- Best paper award of TABLEAUX for Publication on differential dynamic logic, the theory behind KeYmaera [41]
- Publication on differential temporal dynamic logic, a temporal extension of the theory behind KeYmaera, has appeared at LFCS in LNCS [42]
- First brief overview of differential dynamic logic at HSCC in LNCS [43]
- Publication on nominal variant of differential dynamic logic at HyLo'06 [44]