KeYmaeraD: Distributed Theorem Prover for Distributed Hybrid Systems

Discontinued
KeYmaeraD has been replaced by corresponding features in KeYmaera and KeYmaera X, respectively.
Table of Contents
  1. Overview
  2. Case Studies
  3. Download
  4. Developers
  5. Statistics
  6. Selected Publications

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 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 | 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-Verlag Errata fixed in author's version
    [bib | pdf | doi | tool | study | 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-Verlag
    [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-Verlag
    [bib | pdf | doi | slides | TR | LMCS'12 | abstract]

  7. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
    [bib | book | eBook | doi | web]

  8. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pp. 309-352, 2010. © The author
    Special issue for selected papers from TABLEAUX'07. Advance Access published on November 18, 2008 by Oxford University Press.
    [bib | pdf | doi | study | abstract]

  9. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pp. 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

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.