KeYmaera X: Documentation

Table of Contents
  1. Documentation
  2. Using KeYmaera X
  3. Tool Architecture
  4. Selected Publications
Download or try
Online or consult
API Doc or study
Source

Documentation

Cheat Sheet or
FM tutorial or
LICS tutorial or
LICS slides or
STTT tutorial or
Lecture Notes or
Lecture Videos or
Wiki or
API Doc or
Source or
Book or
CPSWEEK tutorial or
FMCAD tutorial

Using KeYmaera X

KeYmaera X getting started video on YouTube

After starting KeYmaera X, usage information can be obtained from the Help menu on the top right. The first thing you want to do is select your favorite arithmetic solver from the menu Help->Backend Tool Configuration. At present, the support for Mathematica provides more functionality than that of Z3 which ships with KeYmaera X.

Tactics are used extensively in the implementation of KeYmaera X. One way to learn how KeYmaera X tactics work is to observe how KeYmaera X automatically generates a tactic for you as you interact with a proof. To demonstrate some of the functionalities of tactics, custom tactics are also included for the tutorial models.

  1. Open the Models page in the menu.
  2. Click on Browse in the tactics column for one of the models.
  3. Click Prove associated model.
These examples are also provable directly with much simpler tactics or fully automatically. But the custom tactics demonstrate different features and give a good idea on the structure of the resulting proof.

Tool Architecture

KeYmaera X was designed to achieve powerful automation of hybrid systems theorem proving while ensuring soundness. The architecture of KeYmaera X is separated into a small, soundness-critical kernel and an extensive tactic framework to regain and exceed the convenience of powerful proof rules.
KeYmaera X is powered by multidynamics technology.

Selected Publications

The differential dynamic logic [2,9] and proof calculus that KeYmaera X implements are described in detail [13,18]. The KeYmaera X theorem prover itself is described in a tool paper [14]. A tutorial on the modeling language that KeYmaera X uses can be found in STTT [12]. A tutorial on differential dynamic logic and its proof principles in LICS [9].
  1. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
    Change and delay contracts for hybrid system component verification.
    In Marieke Huisman and Julia Rubin, editors, Fundamental Approaches to Software Engineering. FASE 2017, volume 10202 of LNCS, pp. 134-151. Springer, 2017. © Springer-Verlag
    [bib | pdf | doi]

  2. Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer.
    Formally verified differential dynamic logic.
    Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, Paris, France, January 16-17, 2017, pp. 208-221, ACM, 2017. © ACM
    [bib | pdf | doi | Isabelle | Coq]

  3. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
    A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system.
    STTT, 2016.
    Special issue for selected papers from TACAS'15. © Springer-Verlag
    [bib | pdf | doi | study | TACAS'15]

  4. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning, 2016. © The author
    [bib | pdf | doi | arXiv]

  5. Stefan Mitsch and André Platzer.
    ModelPlex: Verified runtime validation of verified cyber-physical system models.
    Formal Methods in System Design, 49(1), pp. 33-74. 2016.
    Special issue for selected papers from RV'14. © The authors
    [bib | pdf | doi | RV'14]

  6. André Platzer.
    Logic & proofs for cyber-physical systems.
    In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings, volume 9706 of LNCS, pp. 15-21. Springer, 2016. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | slides]

  7. Nathan Fulton and André Platzer.
    A logic of proofs for differential dynamic logic:
    Toward independently checkable proof certificates for dynamic logics.
    In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 2016 Conference on Certified Programs and Proofs, CPP 2016, St. Petersburg, FL, USA, January 18-19, 2016, pp. 110-121. ACM, 2016. © ACM
    [bib | pdf | doi | slides]

  8. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer.
    KeYmaera X: An aXiomatic tactical theorem prover for hybrid systems.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015. © Springer-Verlag
    [bib | pdf | doi | slides | poster | tool]

  9. André Platzer.
    A uniform substitution calculus for differential dynamic logic.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467-481. Springer, 2015. © Springer-Verlag
    [bib | pdf | doi | slides | arXiv]

  10. Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
    How to model and prove hybrid systems with KeYmaera: A tutorial on safety.
    STTT, 18(1), pp. 67-91, 2016. © Springer-Verlag
    [bib | pdf | doi]

  11. André Platzer.
    Differential game logic.
    ACM Trans. Comput. Log. 17(1), pp. 1:1-1:52, 2015. © The author
    [bib | pdf | doi | arXiv]

  12. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv:1205.4788, May 2012.
    [bib | pdf | arXiv]

  13. André Platzer.
    Logics of dynamical systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 13-24. IEEE 2012. © IEEE
    Invited paper.
    [bib | pdf | doi | slides]

  14. André Platzer.
    The complete proof theory of hybrid systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541-550. IEEE 2012. © IEEE
    [bib | pdf | doi | slides | TR]

  15. André Platzer.
    The structure of differential invariants and differential cut elimination.
    Logical Methods in Computer Science, 8(4), pp. 1-38, 2012. © The author
    [bib | pdf | doi | eprint | arXiv]

  16. André Platzer.
    Logic and compositional verification of hybrid systems.
    In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pp. 28-43. Springer, 2011. © Springer-Verlag
    Invited tutorial.
    [bib | pdf | doi | slides]

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

  18. André Platzer.
    Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems.
    PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
    ACM Doctoral Dissertation Honorable Mention Award in 2009.
    Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
    [bib | pdf | eprint | book | doi | web | slides]

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

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

  21. 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, pp. 216-232. Springer, 2007. © Springer-Verlag
    This paper was awarded the TABLEAUX Best Paper Award.
    [bib | pdf | doi | slides | study | TR]

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.

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.