KeYmaera User Tutorial
- How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety
- Tutorial examples: start KeYmaera and choose File->Load Project in its menu and select the project KeYmaera Tutorial
- Video tutorials
This paper is a tutorial 
on how to model and prove complex properties of complex hybrid systems in
Keywords: formal verification of hybrid systems, differential dynamic logic, automated theorem proving, introduction to hybrid system modeling and verification
Selected PublicationsThe canonical references on the KeYmaera approach are  and . The most comprehensive description of the KeYmaera approach can be found in the book . Also see the publication reading guide.
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. © The authors
[bib | ✂ | pdf | doi | mypdf | abstract]
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
[bib | ✂ | pdf | doi | slides | abstract]
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]
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 | abstract]
André Platzer and Jan-David Quesel.
KeYmaera: A hybrid theorem prover for hybrid systems.
In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171-178. Springer, 2008. © Springer
[bib | ✂ | pdf | doi | slides | tool | abstract]
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]
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning 41(2), pp. 143-189, 2008. © The author
[bib | ✂ | pdf | doi | mypdf | study | abstract]
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
This paper was awarded the TABLEAUX Best Paper Award.
[bib | ✂ | pdf | doi | slides | study | TR | abstract]