KeYmaera: A Hybrid Verification Tool for Hybrid Systems

Overview

Download 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.

KeYmaera is a deductive verification tool for hybrid systems. It is an automated theorem prover implementing the calculus for the differential dynamic logic (dL) for verifying hybrid systems. KeYmaera extends the KeY tool with Mathematica and corresponding algorithms and proof strategies such that it can be used for practical verification of hybrid systems with support for symbolic parameters.

KeYmaera is a theorem prover with significant automation (95% to 100%) and corresponding automatic proof strategies. It contains differential equation handling and an integration of full first-order real arithmetic into the theorem prover. For discovery of invariants and parametric safety constraints, KeYmaera also provides interactive techniques, proof browsing and proof reuse. The GUI of KeYmaera can be used to navigate and manipulate the proofs discovered by KeYmaera proof strategies. The graphical user interface of KeYmaera looks as follows:

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.

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:

• 30.01.2008: added automatic invariant discovery procedure
• 30.01.2008: improved automated handling of existentially quantified properties
• 30.01.2008: user interface improvements
• 30.01.2008: KeYmaera now supports proof @annotations.
• 19.11.2007: Improved and faster quantifier handling.
• 19.11.2007: Transition system views can be generated automatically, e.g., the ETCS transition system example.

Download & Documentation

• Download KeYmaera
• User Guide & Tutorial for KeYmaera
• KeYmaera mailing list

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

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, LNCS, Springer-Verlag, 2008. (c) Springer Verlag
[bib]

[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, LNCS, Springer-Verlag, 2008. (c) Springer Verlag
[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,, LNCS, Springer-Verlag, 2008. (c) Springer Verlag
[bib]

[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]