|
|
Download
or
Launch
KeYmaera
|
Overview
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies.
It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems.
KeYmaera supports differential dynamic logic (dL), which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata.
For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically.
To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy.
Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.
|
|
 |
The KeYmaera verification tool provides significant automation (up to 100%).
It handles differential equations and integrates full first-order real arithmetic.
For discovery of invariants and parametric safety constraints, KeYmaera also provides
interactive techniques, proof browsing, proof reuse, and proof annotations.
The graphical user interface of KeYmaera can be used to navigate and manipulate the proofs
discovered by KeYmaera.
Case Studies
The KeYmaera verification tool has been used very successfully to automatically verify
collision avoidance for the cooperation layer of fully parametric European Train Control System (ETCS).
It has also been used to derive the required safety constraints on the free parameters of ETCS.
Recent case studies are verified aircraft collision avoidance maneuvers: the tangential roundabout maneuvers.
Some academic standard examples from the hybrid systems world have been verified with KeYmaera as well, including a fully parametric version of the bouncing ball and the standard, non-parametric water tank.
For more details on case studies see KeYmaera examples.
KeYmaera Tool Architecture
The architecture of the KeYmaera verification tool has a plug-in system for solvers and proof rules
and allows to adjust the automatic proof strategies by several options.
News
KeYmaera is actively developed and maintained.
Thus, the set of features and the download version are updated continuously.
Recently released additions to KeYmaera include:
- 05/28/2009: New KeYmaera Installer with simplified setup
- 05/01/2009: Several improvements and bugfixes for the KeYmaera Webstart and KeYmaera Download
- 04/21/2009: Carnegie Mellon University press release regarding Cyber-Physical Systems Verification
- 03/18/2009: Major improvements in KeYmaera Webstart Version, which now supports Mathematica, Reduce/Redlog and QEPCAD B as optional solvers
- 03/18/2009: Simplified configuration management in KeYmaera
- 03/06/2009: Improved the KeYmaera Webstart Version
- 03/06/2009: Add while loop statement to hybrid programs
- 03/05/2009: Significant advances in automation and integration
- 03/05/2009: Built-in Gröbner Bases and Fourier-Motzkin elimination
- 03/05/2009: Interface with Redlog as a new optional background solver
- 03/05/2009: Improve integration of QEPCAD B as a background solver
- 03/05/2009: Interface with Gröbner Bases in built-in Orbital library
- 03/05/2009: Interface with CSDP as a background solver
- 01/28/2009: Several strategy and automation improvements
- 01/28/2009: Improved handling of real arithmetic
- 01/20/2009: New system specification language features
- 09/09/2008: Improved the KeYmaera Webstart Version with native QEPCAD support
- 09/08/2008: Release KeYmaera 1.4.1
- 08/21/2008: KeYmaera now provides a brand new project assistant: click File->Load Project
- 08/21/2008: Interface QEPCAD B as a new background solver alternative for Mathematica
- 08/21/2008: Introduce differential inequality and differential inclusion handling
- 08/21/2008: Add differential refinement support for differential constraints
- 08/21/2008: Faster tool startup
- 08/20/2008: Background article on the logic behind KeYmaera has appeared in Journal of Automated Reasoning
- 08/19/2008: Slides on KeYmaera Tool
- 06/27/2008: Improved the KeYmaera Webstart Version
- 06/27/2008: Better proof presentation and rendering
- 06/13/2008: Equational Gröbner basis verification support
- 06/13/2008: Built-in arithmetical simplifier support
- 06/13/2008: Improved prover automation
- 01/30/2008: Added automatic invariant and differential invariant discovery procedure
- 06/13/2008: Support differential invariants
- 01/30/2008: Improved automated handling of existentially quantified properties
- 01/30/2008: User interface improvements
- 01/30/2008: KeYmaera now supports proof @annotations.
- 11/19/2007: Improved and faster quantifier handling.
- 11/19/2007: Transition system views can be generated automatically, e.g., the ETCS transition system example.
- 07/10/2007: Slides on differential dynamic logic
Download, Documentation & Tutorial
Statistics
KeYmaera is based on the KeY system
and Mathematica.
Including the graphical user interface, the KeYmaera verification tool has
- 206,000 SLOC (Source Lines of Code, i.e., not counting comments), generated using David A. Wheeler's 'SLOCCOUNT'
- 4800 Java classes
- 141 proof rules consisting of
- 37 symbolic decomposition rules for hybrid systems, and
- 104 rules for handling first-order real arithmetic and propositional logic, with various optimizations.
Etymology: The Name KeYmaera
KeYmaera is a hybrid version of the KeY tool.
It amalgamates deductive and continuous reasoning.
Thus, it is a hybrid mixture of continuous, algebraic, and deductive techniques.
And doubly so, because KeYmaera is for verifying hybrid systems.
Consequently, our tool truly is a
chimaera of KeY and continuous maths
for hybrid systems, which is why we call it KeYmaera.
In classical Greek mythology, Chimaera (Χíμαιρα)
is a hybrid mixture of multiple animals.
KeYmaera, instead, is a hybrid mixture of multiple proving technologies
from logic or discrete and continuous mathematics and KeYmaera is intended for hybrid systems verification, which are systems evolving along mixed discrete and continuous transitions.
The development code name for KeYmaera was HyKeY,
because HyKeY stands to reason as a canonical
name in line with hybrid systems model checkers like
HyTech or
HySAT.
We decided to go for a fancy name instead, paying homage to KeYmaera's roots in a hybrid extension of KeY, to its purpose for hybrid systems verification, and to the hybrid nature of its algorithmic design combining aspects of theorem proving, computer algebra, decision procedures, and model checking.
Abstract
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies.
It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems.
KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata.
For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically.
To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy.
Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.
Keywords:
dynamic logic, sequent calculus, automated theorem proving, decision procedures, computer algebra, verification of parametric hybrid systems, quantifier elimination
-
André Platzer, Jan-David Quesel, and Philipp Rümmer.
Real World Verification.
In Renate A. Schmidt, editor,
International Conference on Automated Deduction, CADE'09, Montreal, Canada, Proceedings,
volume 5663 of LNCS, pages 485-501. Springer, 2009.
(c) Springer Verlag
[bib
| pdf]
-
André Platzer and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
Formal Methods in System Design, 2009.
Accepted for publication; 23 pages.
(c) Springer Verlag
[bib
| pdf
| doi]
-
André Platzer and Jan-David Quesel.
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems.
In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors,
Automated Reasoning, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings,
volume 5195 of LNCS, pages 171-178. Springer, 2008.
(c) Springer Verlag
[bib
| pdf
| doi
| slides]
-
André Platzer and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
In Aarti Gupta and Sharad Malik, editors,
Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings,
volume 5123 of LNCS, pages 176-189, Springer, 2008.
(c) Springer Verlag
[bib
| pdf
| doi]
-
André Platzer and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
School of Computer Science, Carnegie Mellon University,
CMU-CS-08-103, Feb, 2008.
[bib
| pdf]
-
André Platzer and Jan-David Quesel.
Logical Verification and Systematic Parametric Analysis in Train Control.
In Magnus Egerstedt and Bud Mishra, editors,
Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings,
volume 4981 of LNCS, pages 646-649. Springer, 2008.
(c) Springer Verlag
[bib
| pdf
| doi]
-
André Platzer.
Differential-algebraic Dynamic Logic for Differential-algebraic Programs.
Journal of Logic and Computation, 2008.
Accepted for publication by Oxford University Press; 44 pages.
[bib
| pdf
| doi]
-
André Platzer.
Differential Dynamic Logic for Hybrid Systems.
Journal of Automated Reasoning, 41(2), pages 143-189, 2008.
(c) Springer Verlag
[bib
| pdf
| doi]
-
André Platzer.
Combining Deduction and Algebraic Constraints for Hybrid System Analysis.
In Bernhard Beckert, editor,
4th International Verification Workshop, VERIFY'07,
Workshop at Conference on Automated Deduction (CADE),
Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
[bib
| pdf]
-
André Platzer.
Differential dynamic logic for verifying parametric hybrid systems.
In Nicola Olivetti, editor,
Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007,
Aix en Provence, France, July 3-6, 2007, Proceedings,
volume 4548 of LNCS, pages 216-232. Springer, 2007.
(c) Springer Verlag
This paper was awarded the Tableaux Best Paper Award.
[bib
| pdf
| doi
| slides]
-
André Platzer.
A temporal dynamic logic for verifying hybrid system invariants.
In Sergei Artemov and Anil Nerode, editors,
Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings,
volume 4514 of LNCS, pages 457-471. Springer, 2007.
(c) Springer Verlag
[bib
| pdf
| doi
| slides]
-
André Platzer.
Differential logic for reasoning about hybrid systems.
In Alberto Bemporad, Antonio Bicchi, and Giorgio Buttazzo, editors,
Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings,
volume 4416 of LNCS, pages 746-749. Springer, 2007.
(c) Springer Verlag
[bib
| pdf
| doi]
More details on the differential dynamic logic (dL),
on the hybrid program model for hybrid systems,
and on the principles of logic for hybrid systems.
For full details, please see
more publications.
|
