KeYmaera: A Hybrid Theorem Prover for Hybrid Systems

Table of Contents
Overview Case Studies KeYmaera Tool Architecture News Verification Download, Documentation & Tutorial Statistics Etymology: The Name KeYmaera Abstract Selected Publications

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) [16][14], 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 [15][6]. 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 [3] and air traffic management [4].

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 provides automatic procedures [10][7], but also 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 [3]. KeYmaera has also been used to verify collision avoidance in aircraft collision avoidance maneuvers [4]. 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 [8] 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 [8] and allows to adjust the automatic proof strategies by several options.

News

KeYmaera is actively developed and maintained. Its set of features and the download version are updated continuously. Recently released additions to KeYmaera include:

02/01/2010: An article introducing and developing the theory of differential invariants for verification in KeYmaera has appeared in Journal of Logic and Computation [13]
11/05/2009: Best paper award of FM for a publication on formal verification of an aircraft maneuver in KeYmaera [4]
10/19/2009: Read about KeYmaera mentioned in the Brilliant 10 of 2009
10/15/2009: Read about this research in CMU News
10/15/2009: Read about KeYmaera research in Pittsburgh Post-Gazette
10/15/2009: Read about this research in CMU SCS News
09/01/2009: Publications on case studies in formal verification of hybrid systems in KeYmaera available [4][3]
08/19/2009: Announced NSF Expedition on CMACS
07/26/2009: Publication on advanced real arithmetic handling in KeYmaera has appeared at CADE [6]
07/10/2009: Background article on algorithmic computation of differential invariants has appeared in Formal Methods in System Design [7]
06/29/2009: Started KeYmaera FAQ
06/01/2008: Release KeYmaera 1.5
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
11/18/2008: Background article on extended logics behind KeYmaera introducing differential invariants has appeared in Journal of Logic and Computation advance access [13]
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 [13]
08/21/2008: Add differential refinement support for differential constraints [13]
08/21/2008: Faster tool startup
08/20/2008: Background article on the logic behind KeYmaera has appeared in Journal of Automated Reasoning [14]
08/19/2008: Slides on KeYmaera Tool [8]
08/10/2008: KeYmaera tool paper appeared at IJCAR in LNCS [8]
07/05/2008: Publication on algorithmic computation of differential invariants appeared at CAV [10] based on the theory in [13]
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 [10]
06/13/2008: Support differential invariants [13]
01/30/2008: Improved automated handling of existentially quantified properties [14]
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/15/2007: Publication on proof procedures and deduction modulo theory in KeYmaera at VERIFY [15]
07/10/2007: Slides on differential dynamic logic [16]
07/04/2007: Best paper award of TABLEAUX for Publication on differential dynamic logic, the theory behind KeYmaera [16]
06/04/2007: Publication on differential temporal dynamic logic, a temporal extension of the theory behind KeYmaera, has appeared at LFCS in LNCS [17]
04/04/2007: Publication on first plans for differential dynamic logic at HSCC in LNCS [18]
08/11/2006: Publication on nominal variant of differential dynamic logic at HyLo [19]

Verification

In KeYmaera, verifying correct functioning of hybrid systems amounts to proving corresponding formulas in, what is called, differential dynamic logic dL [16][14]. These formulas state the desired correctness properties of the hybrid systems under consideration, including safety, liveness, reactivity, and controllability properties. For showing that these systems operate as expected, André Platzer has devised a logical verification calculus [16][14].

Advanced verification technology for differential dynamic logics is further based on differential invariants [16][10][7], which are formulas that remain true along the dynamics of the hybrid system and its differential equations. Differential invariants and differential induction are essentially a generalization of discrete induction to differential equations. This verification technology for differential dynamic logic has been implemented in the KeYmaera theorem prover for hybrid systems.

KeYmaera implements the verification calculi for the logics described in [16][14][17][13] The verification algorithms implemented in KeYmaera further include [15][6], also see the KeYmaera tool paper [8].

Download, Documentation & Tutorial

Download KeYmaera for installation on your computer
User Guide & Tutorial for KeYmaera
KeYmaera FAQ - Frequently Asked Questions
KeYmaera mailing list
KeYmaera feature request & bug tracker

Statistics

KeYmaera is based on the KeY system and on computer algebra tools like Mathematica, Reduce, and the Orbital library. Including the graphical user interface, the KeYmaera verification tool has

206,000 SLOC (Source Lines of Code, i.e., not counting comments), counted 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 [16][14], 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

André Platzer.
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
Springer, 2010. To appear.
[bib | web]
André Platzer.
Differential dynamic logic: Automated theorem proving for hybrid systems.
Künstliche Intelligenz, 2010.
Invited paper. (c) Springer Verlag
[bib | doi]
André Platzer and Jan-David Quesel.
European Train Control System: A case study in formal verification.
In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009. (c) Springer Verlag
[bib | pdf | doi | slides | study]
André Platzer and Edmund M. Clarke.
Formal verification of curved flight collision avoidance maneuvers: A case study.
In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pages 547-562. Springer, 2009. (c) Springer Verlag
This paper was awarded the FM Best Paper Award.
[bib | pdf | doi | slides]
André Platzer.
Verification of cyberphysical transportation systems.
IEEE Intelligent Systems, 24(4), pages 10-13, Jul/Aug, 2009. (c) IEEE.
Invited paper.
[bib | doi]
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
Introduces a decision procedure for nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the real Nullstellensatz.
[bib | pdf | doi]
André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods in System Design, 35(1), pages 98-120, 2009. (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.
Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems.
PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
To appear with Springer as Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
[bib]
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, 20(1), pages 309-352, 2010. Advance Access published on November 18, 2008 by Oxford University Press.
[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]
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 | 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.