
Download
or consult API Doc or study Source 
Documentation
Using KeYmaera X
 Models: displays preinstalled models, clicking "Show Proofs" takes you to the proofs for a specific model.
 Proofs: displays preinstalled proofs, clicking "Load" checks the proof, when done "Open" takes you to the proof.
Tactics are used extensively in the implementation of KeYmaera X. To demonstrate some of the functionalities of tactics, we included detailed custom tactics for all example models. The steps for running a tactic on a model follow:
 Open the "Models" page from the dashboard.
 Click on "Browse" in the tactics column for one of the models. A modal dialog will appear containing a tactic; copy the tactic onto your clipboard.
 Close the modal dialog and click on "Show Proofs" for the associated model. Start a new proof.
 Paste the tactic into the Tactic Combinator Language Term box, and click "Run Custom Tactic". Be sure not to doubleclick.
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.Selected Publications
The differential dynamic logic [2,9] and proof calculus that KeYmaera X implements are described in detail [13,17]. 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].
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, ACM, 2017. © ACM
[bib  pdf  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, 2016.
Special issue for selected papers from TACAS'15. © SpringerVerlag
[bib  pdf  doi  study  TACAS'15]

André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning, 2016. © 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]

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, 2010. 426 p. ISBN 9783642145087.
[bib  book  eBook  doi  web]

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]

André Platzer.
Differentialalgebraic dynamic logic for differentialalgebraic programs.
Journal of Logic and Computation, 20(1), pp. 309352, 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]

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]