| Table of Contents |
|---|
Outdated: Use Successor KeYmaera X Instead
The successor, KeYmaera X, is an entirely new and overall better theorem prover for hybrid systems building on the experience with the successes of KeYmaera and KeYmaeraD. For hybrid systems verification, you should use the new KeYmaera X prover instead. If you are looking for distributed hybrid systems verification the older KeYmaera prover is more suitable.
Overview
Distributed hybrid systems present extraordinarily challenging problems for verification. On top of the notorious difficulties associated with distributed systems, they also exhibit continuous dynamics described by quantified differential equations. All serious proofs rely on decision procedures for real arithmetic, which can be extremely expensive. Quantified differential dynamic logic (QdL) [4] has been identified as a promising approach for getting a handle in this domain. We address the problem of automated theorem proving for distributed hybrid systems. We have designed a powerful strategy and tactics language for directing proof search. With these techniques, we have implemented a new automated theorem prover called KeYmaeraD. To overcome the high computational complexity of distributed hybrid systems verification, KeYmaeraD uses a distributed proving backend. We have experimentally observed that calls to the real arithmetic decision procedure can effectively be made in parallel.
Keywords: quantified differential dynamic logic, verification of distributed hybrid systems, sequent calculus, automated theorem proving, distributed theorem proving, decision procedures, computer algebra, quantifier elimination
Case Studies
In conjunction with KeYmaera, the KeYmaeraD verification tool has been used successfully for verification in medical surgical robotics applications for skull base surgery [9] and in proving collision freedom of flyable disc maneuvers for an arbitrary number of aircraft [8]. |
 |
|
 |
||
Download
KeYmaeraD is an open source verification tool written in Scala 2.9 and compiled into the platform-neutral JVM. Download KeYmaeraD source code and compile to run.
Developers
KeYmaeraD has been developed in the group of Prof. André Platzer at Carnegie Mellon University. The main KeYmaeraD developers are
- André Platzer, Carnegie Mellon University
- David Renshaw, Carnegie Mellon University (lead developer)
- Ping Hou, Carnegie Mellon University (KeY parser)
Statistics
KeYmaeraD is implemented in Scala, which compiles to JVM bytecode. KeYmaeraD has
- 7,000 SLOC (Source Lines of Code, i.e., not counting comments), counted using David A. Wheeler's 'SLOCCOUNT'
- KeYmaeraD compiles into 1,400 classes of JVM bytecode
Selected Publications
The canonical reference on logic and proof calculi for distributed hybrid systems is [4]. Quantified differential invariants are described in [5]. A major case study for quantified differential dynamic logic is reported in [6]. Also see publications on distributed hybrid systems logic and the publication reading guide.-
Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 263-272. ACM, 2013. © ACM
[bib | ⧉ | pdf | doi | slides | study | abstract]
-
Sarah M. Loos, David W. Renshaw and André Platzer.
Formal verification of distributed aircraft controllers.
In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 125-130. ACM, 2013. © ACM
[bib | ⧉ | pdf | doi | slides | poster | study | TR | abstract]
-
David W. Renshaw, Sarah M. Loos and André Platzer.
Distributed theorem proving for distributed hybrid systems.
In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pp. 356-371. Springer, 2011. © Springer
[bib | ⧉ | pdf | doi | tool | study | errata | abstract]
-
Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive cruise control:
Hybrid, distributed, and now formally verified.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 42-56. Springer, 2011. © Springer
[bib | ⧉ | pdf | doi | slides | study | TR | abstract]
-
André Platzer.
Quantified differential invariants.
In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, pp. 63-72. ACM, 2011. © ACM
[bib | ⧉ | pdf | doi | slides | abstract]
-
André Platzer.
Quantified differential dynamic logic for distributed hybrid systems.
In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pp. 469-483. Springer, 2010. © Springer
[bib | ⧉ | pdf | doi | slides | TR | LMCS'12 | abstract]
-
André Platzer.
Logical Analysis of Hybrid Systems:
Proving Theorems for Complex Dynamics.
Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
[bib | ⧉ | doi | book | web | errata | abstract]
-
André Platzer.
Differential-algebraic dynamic logic for differential-algebraic programs.
Journal of Logic and Computation 20(1), pp. 309-352, 2010.
Special issue for selected papers from TABLEAUX'07. © The author
[bib | ⧉ | pdf | doi | eprint | study | errata | TABLEAUX'07 | abstract]
-
André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning 41(2), pp. 143-189, 2008. © The author
[bib | ⧉ | pdf | doi | mypdf | study | abstract]
 |
Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.