Overview
|
Download
or
Launch
KeYmaera
|
|
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 water tank.
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.
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:
- 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 discovery procedure
- 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.
Download, Documentation & Tutorial
Statistics
KeYmaera is based on the KeY system
and Mathematica.
Including the graphical user interface, the KeYmaera verification tool has
- 186,000 SLOC (Source Lines of Code, i.e., not counting comments)
- 4428 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.
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.
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
Selected Publications
- [PQ08b]
-
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-Verlag, 2008.
(c) Springer Verlag
[bib
| pdf]
- [PQ08a]
-
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-Verlag, 2008.
(c) Springer Verlag
[bib
| pdf]
- [Pla08]
-
André Platzer.
Differential Dynamic Logic for Hybrid Systems.
Journal of Automated Reasoning, 2008.
Accepted for publication.
[bib
| pdf]
- [PC08]
-
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]
- [Pla07d]
-
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]
- [Pla07c]
-
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
| slides]
- [Pla07b]
-
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
| slides]
- [Pla07a]
-
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-Verlag, 2007.
(c) Springer Verlag
[bib
| pdf]
- [Pla06]
-
André Platzer.
Towards a hybrid dynamic logic for hybrid dynamic systems.
In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva, and Jørgen Villadsen, editors,
Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA,
Electr. Notes Theor. Comput. Sci. 174(6):63-77, 2007.
[bib
| pdf]
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 on related publications, please see
more publications.
|
