KeYmaeraD: Distributed Theorem Prover for Distributed Hybrid Systems

  1. Home
  2. >>
  3. Tools
  4. >>
  5. Extra Tools
  6. >>
  7. KeYmaeraD
Table of Contents
  1. Outdated: Use Successor KeYmaera X Instead
  2. Overview
  3. Case Studies
  4. Download
  5. Developers
  6. Statistics
  7. Selected Publications

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.

 

See Successor: KeYmaera X

 

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

With contributions from

Statistics

KeYmaeraD is implemented in Scala, which compiles to JVM bytecode. KeYmaeraD has

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.
  1. 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]

  2. 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]

  3. 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]

  4. 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]

  5. 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]

  6. 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]

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

  8. 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]

  9. 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]

Copyright of publications is with the publisher or author as indicated. Author's versions of papers are posted with permission of the publisher for your personal use. Not for redistribution or commercial purpose. Slides are copyright © by the author. All information and materials on this site are provided solely for informational purposes on an AS-IS basis, and any and all implied warranties are expressly disclaimed. More details on the quantified differential dynamic logic (QdL), on the quantified hybrid program model for distributed hybrid systems. For full details, please see more publications.

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.