
⇓ Download
or get Source or read Book or watch Videos 
Documentation
Using KeYmaera X
After starting KeYmaera X and signing in, usage information can be obtained from the Help menu on the top right. You also always have the button ? for quick help.
 Quick usage help: display help with the ? menu button on each page.
User Tutorial Video
Firsttime Setup
 When the KeYmaera X Prover opens for the first time in the web browser, register a new user name and password for your logical proof storage database. Choose a password that you are not using anywhere else.
 Configure your arithmetic solver from the menu KeYmaera X→Preferences and choose Save Configuration. At present, the support for Mathematica and Wolfram Engine provide more functionality than that of Z3 which ships with KeYmaera X.
 To get started you may want to import the textbook examples by going to menu KeYmaera X→Models and then select Import for the LFCPS 2018 Textbook collection.
Models
KeYmaera X→Models menu entry displays your CPS models. Import models from tutorials or load your own models with KeYmaera X→New Model. Choose an action to show or start proofs for a specific model, generate monitors, code, or test cases. As a simple example, remember the bouncing ball from your childhood days.
[KeYmaera X Model]
Proofs
KeYmaera X→Proofs menu entry displays all CPS proofs that you've completed or started. Choose an action to open or export a proof. You can start a new proof by selecting the action Start Proof on your favorite model listed from the KeYmaera X→Proofs menu entry.
Tactics
Tactics are used extensively in the implementation of KeYmaera X. They are also useful to customize proof search for a model. 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. Select the Tactic tab at any time while proving a model to see what tactic program would have performed the same proof you just did per hand.
Several of the tutorial examples also come with a range of different styles of tactics that prove them.
 Click KeYmaera X→Models menu entry.
 Click on Browse in the tactics column for one of the models.
 Click Prove associated model.
The tactics language Bellerophon and its tactic library is also described in the ScalaDoc API.
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, soundnesscritical kernel and an extensive tactic framework to regain and exceed the convenience of powerful proof rules.How to Cite KeYmaera X
There are many papers about KeYmaera X. Its theory and proof calculus are described in JAR'17:
André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning, 59(2), pp. 219265, 2017. © The author
[bib  pdf  doi  arXiv]

Nathan Fulton, Stefan Mitsch, JanDavid 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. 527538. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  poster  tool]

André Platzer.
Logical Foundations of CyberPhysical Systems.
Springer, Cham, 2018. 659 pages. ISBN 9783319635873.
[bib  doi  slides  video  book  web  errata]

Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
Bellerophon: Tactical theorem proving for hybrid systems.
In Mauricio AyalaRincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207224. Springer, 2017. © SpringerVerlag
[bib  pdf  doi  slides  kyx]

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

André Platzer and Yong Kiam Tan.
Differential equation axiomatization:
The impressive power of differential ghosts.
In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 819828. ACM 2018. © The authors
[bib  pdf  doi  slides  arXiv]

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
VeriPhy: Verified controller executables from verified cyberphysical system models.
In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617630. ACM 2018. © The authors
[bib  pdf  doi  slides  video  tool]

Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
Pegasus: A framework for sound continuous invariant generation.
In Maurice ter Beek, Annabelle McIver, and José N. Oliviera, editors, FM 2019: Formal Methods  The Next 30 Years, volume 11800 of LNCS, pp. 138157. Springer, 2019. © Springer
This paper was awarded the FM Best Tool Paper Award.
[bib  pdf  doi  slides  tool]
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] and its tactics language Bellerophon at ITP [22]. 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 appeared at LICS [9]. A comprehensive introduction into the core principles of cyberphysical systems, including their modeling and proving principles can be found in a textbook [23].
Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
Pegasus: A framework for sound continuous invariant generation.
In Maurice ter Beek, Annabelle McIver, and José N. Oliviera, editors, FM 2019: Formal Methods  The Next 30 Years, volume 11800 of LNCS, pp. 138157. Springer, 2019. © Springer
This paper was awarded the FM Best Tool Paper Award.
[bib  pdf  doi  slides  tool]

Brandon Bohrer, Manuel Fernández and André Platzer.
dL_{ɩ} Definite descriptions in differential dynamic logic.
In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 94110. Springer, 2019. © SpringerVerlag
[bib  pdf  doi  slides  TR]

André Platzer.
Uniform substitution at one fell swoop.
In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425441. Springer, 2019. © The author
[bib  pdf  doi  slides  Isabelle  arXiv]

André Platzer and Yong Kiam Tan.
Differential equation axiomatization:
The impressive power of differential ghosts.
In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 819828. ACM 2018. © The authors
[bib  pdf  doi  slides  arXiv]

André Platzer.
Uniform substitution for differential game logic.
In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, Oxford, UK, Proceedings, volume 10900 of LNCS, pp. 211227. Springer 2018. © SpringerVerlag
[bib  pdf  doi  slides  arXiv]

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
VeriPhy: Verified controller executables from verified cyberphysical system models.
In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617630. ACM 2018. © The authors
[bib  pdf  doi  slides  video  tool]

Nathan Fulton and André Platzer.
Safe reinforcement learning via formal methods:
Toward safe control through proof and learning.
In Sheila A. McIlraith and Kilian Q. Weinberger, editors, AAAI Conference on Artificial Intelligence, pp. 64856492. AAAI 2018. © AAAI Press
[bib  pdf  eprint  slides]

Stefan Mitsch, Marco Gario, Christof J. Budnik, Michael Golm and André Platzer.
Formal verification of train control with air pressure brakes.
In Alessandro Fantechi, Thierry Lecomte and Alexander Romanovsky, editors, RSSRail 2017: Reliability, Safety, and Security of Railway Systems, volume 10598 of LNCS, pp. 173191. Springer, 2017. © SpringerVerlag
[bib  pdf  doi  slides]

Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
Formal verification of obstacle avoidance and navigation of ground robots.
International Journal of Robotics Research. 36(12), pp. 13121340, 2017. © The authors
[bib  pdf  doi  kyx  arXiv]

André Platzer.
Logical Foundations of CyberPhysical Systems.
Springer, Cham, 2018. 659 pages. ISBN 9783319635873.
[bib  doi  slides  video  book  web  errata]

Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
Bellerophon: Tactical theorem proving for hybrid systems.
In Mauricio AyalaRincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207224. Springer, 2017. © SpringerVerlag
[bib  pdf  doi  slides  kyx]

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. 134151. Springer, 2017. © SpringerVerlag
[bib  pdf  doi  slides  study  STTT'18]

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 1617, 2017, pp. 208221, ACM, 2017. © ACM
[bib  pdf  doi  slides  Isabelle  Coq]

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
A formally verified hybrid system for safe advisories in the nextgeneration airborne collision avoidance system.
STTT, 19(6), pp. 717741, 2017.
Special issue for selected papers from TACAS'15. © SpringerVerlag
[bib  pdf  doi  kyx  study  TACAS'15]

André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning, 59(2), pp. 219265, 2017. © The author
[bib  pdf  doi  arXiv]

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

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

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 1819, 2016, pp. 110121. ACM, 2016. © ACM
[bib  pdf  doi  slides]

Nathan Fulton, Stefan Mitsch, JanDavid 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. 527538. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  poster  tool]

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. 467481. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  arXiv]

JanDavid 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. 6791, 2016. © SpringerVerlag
[bib  pdf  doi]

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

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

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

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. 541550. IEEE 2012. © IEEE
[bib  pdf  doi  slides  TR]

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

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. 2843. Springer, 2011. © SpringerVerlag
Invited tutorial.
[bib  pdf  doi  slides]

André Platzer.
Logical Analysis of Hybrid Systems:
Proving Theorems for Complex Dynamics.
Springer, Heidelberg, 2010. 426 pages. ISBN 9783642145087.
[bib  doi  book  web  errata]

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  slides  book  ebook]

André Platzer.
Differentialalgebraic dynamic logic for differentialalgebraic programs.
Journal of Logic and Computation, 20(1), pp. 309352, 2010.
Special issue for selected papers from TABLEAUX'07. © The author.
[bib  pdf  doi  eprint  study  errata  TABLEAUX'07]

André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning, 41(2), pp. 143189, 2008. © SpringerVerlag
[bib  pdf  doi  study]

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 36, 2007, Proceedings, volume 4548 of LNCS, pp. 216232. Springer, 2007. © SpringerVerlag
This paper was awarded the TABLEAUX Best Paper Award.
[bib  pdf  doi  slides  study  TR]
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.