KeYmaera X: Publications

  1. KeYmaera X
    2. >>
  2. Paper
Table of Contents
  1. List of Publications
    1. Publication Overview
    2. How to Cite KeYmaera X
    3. Theory: Logical Foundations
    4. Practice: Theorem Proving & Verification
    5. Applications: Techniques & Case Studies
⇓ Download ⇓ or try
Online or get
Source and read
Book and watch
Videos and follow
Tutorial

List of Publications

Publication Overview

The differential dynamic logic [2,8] and proof calculus that KeYmaera X implements are described in detail [13]. The KeYmaera X theorem prover itself is described in a tool paper [1] and its tactics language Bellerophon at ITP [1]. A tutorial on the modeling language that KeYmaera X uses can be found in STTT [1]. A tutorial on differential dynamic logic and its proof principles appeared at LICS [8]. A comprehensive introduction into the core principles of cyber-physical systems, including their modeling and proving principles can be found in a very readable textbook [14]. The most authoritative answer on differential equations proving can be found in JACM [19].

How to Cite KeYmaera X

There are many papers about KeYmaera X. Its theory and proof calculus are described in JAR'17:
  1. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning 59(2), pp. 219-265, 2017. © The author
    [bib | ✂ | pdf | doi | mypdf | arXiv]

The system description for the theorem prover KeYmaera X appeared at CADE'15:
  1. 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-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015. © Springer
    [bib | ✂ | pdf | doi | slides | poster | tool]

A very readable textbook appeared with Springer 2018, with supporting videos:
  1. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | ✂ | doi | slides | video | book | web | errata]

The tactics framework and tactic library is described at ITP'17 and the ScalaDoc API:
  1. Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
    Bellerophon: Tactical theorem proving for hybrid systems.
    In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207-224. Springer, 2017. © Springer
    [bib | ✂ | pdf | doi | slides | kyx]

The canonical reference for controller and model monitors generated by KeYmaera X's ModelPlex is in FMSD'16 based on RV'14:
  1. 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 | mypdf | RV'14]

  2. Stefan Mitsch and André Platzer.
    ModelPlex: Verified runtime validation of verified cyber-physical system models.
    In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of LNCS, pp. 199-214. Springer, 2014. © Springer
    Best paper finalist
    [bib | ✂ | pdf | doi | slides | study | TR | FMSD'16]

Automatic differential equation proving appeared at LICS'18 and JACM'20:
  1. André Platzer and Yong Kiam Tan.
    Differential equation invariance axiomatization.
    J. ACM 67(1), 6:1-6:66, 2020. © The authors
    [bib | ✂ | pdf | doi | mypdf | slides | video | arXiv]

  2. 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. 819-828. ACM 2018. © The authors
    [bib | ✂ | pdf | doi | mypdf | slides | video | arXiv | JACM'20]

The verified toolchain to correctly compile to executables is at PLDI'18:
  1. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
    VeriPhy: Verified controller executables from verified cyber-physical system models.
    In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617-630. ACM 2018. © The authors
    [bib | ✂ | pdf | doi | mypdf | slides | video]

The invariant generator for KeYmaera X is described in FMSD based on FM'19:
  1. Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
    Pegasus: Sound continuous invariant generation.
    Formal Methods in System Design 58(1), pp. 5-41, 2022.
    Special issue for selected papers from FM'19. © The authors
    [bib | ✂ | pdf | doi | tool | arXiv | FM'19]

  2. 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. 138-157. Springer, 2019. © Springer
    FM Best Tool Paper Award.
    [bib | ✂ | pdf | doi | slides | tool | FMSD]

The implicit function definitions package for KeYmaera X is described at IJCAR'22:
  1. James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André Platzer.
    Implicit definitions with differential equations for KeYmaera X (System Description).
    In Jasmin Blanchette, Laura Kovacs and Dirk Pattinson, editors, Automated Reasoning, International Joint Conference, IJCAR 2022, Haifa, Israel, August 7-12, 2022, Proceedings. volume 13385 of LNCS, pp. 723-733. Springer, 2022. © The authors
    [bib | ✂ | pdf | doi | slides | arXiv]

Theory: Logical Foundations

  1. Marvin Brieger, Stefan Mitsch and André Platzer.
    Uniform substitution for dynamic logic with communicating hybrid programs.
    In Brigitte Pientka and Cesare Tinelli, editors, International Conference on Automated Deduction, CADE-29, Rome, Italy, Proceedings, volume 14132 of LNCS, pp. 96-115. Springer, 2023. © The Authors
    [bib | ✂ | pdf | doi | slides | arXiv]

  2. Yong Kiam Tan and André Platzer.
    Deductive stability proofs for ordinary differential equations.
    In Jan Friso Groote and Kim G. Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, Proceedings, Part II, volume 12652 of LNCS, pp. 181–199. Springer, 2021. © The authors
    [bib | ✂ | pdf | doi | mypdf | slides | video | kyx | arXiv]

  3. Yong Kiam Tan and André Platzer.
    An axiomatic approach to existence and liveness for differential equations.
    Formal Aspects of Computing 33(4), pp. 461-518, 2021.
    Special issue for selected papers from FM'19. © The authors
    [bib | ✂ | pdf | doi | arXiv | FM'19]

  4. André Platzer and Yong Kiam Tan.
    Differential equation invariance axiomatization.
    J. ACM 67(1), 6:1-6:66, 2020. © The authors
    [bib | ✂ | pdf | doi | mypdf | slides | video | arXiv]

  5. Yong Kiam Tan and André Platzer.
    An axiomatic approach to liveness for differential equations.
    In Maurice ter Beek, Annabelle McIver, and José N. Oliviera, editors, FM 2019: Formal Methods - The Next 30 Years, volume 11800 of LNCS, pp. 371-388. Springer, 2019. © Springer
    [bib | ✂ | pdf | doi | slides | arXiv | FAC'21]

  6. André Platzer.
    Uniform substitution at one fell swoop.
    In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019. © The author
    [bib | ✂ | pdf | doi | mypdf | slides | Isabelle | arXiv]

  7. 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. 819-828. ACM 2018. © The authors
    [bib | ✂ | pdf | doi | mypdf | slides | video | arXiv | JACM'20]

  8. 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. 211-227. Springer 2018. © Springer
    [bib | ✂ | pdf | doi | slides | arXiv]

  9. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | ✂ | doi | slides | video | book | web | errata]

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

  11. 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 | mypdf | RV'14]

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

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

  14. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
    [bib | ✂ | pdf | arXiv | LICS'12]

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

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

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

  18. André Platzer.
    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]

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

  20. André Platzer.
    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]

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

  22. 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
    TABLEAUX Best Paper Award.
    [bib | ✂ | pdf | doi | slides | study | TR]

Practice: Theorem Proving & Verification

  1. James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André Platzer.
    Implicit definitions with differential equations for KeYmaera X (System Description).
    In Jasmin Blanchette, Laura Kovacs and Dirk Pattinson, editors, Automated Reasoning, International Joint Conference, IJCAR 2022, Haifa, Israel, August 7-12, 2022, Proceedings. volume 13385 of LNCS, pp. 723-733. Springer, 2022. © The authors
    [bib | ✂ | pdf | doi | slides | arXiv]

  2. Yong Kiam Tan, Stefan Mitsch and André Platzer.
    Verifying switched system stability with logic.
    In Ezio Bartocci and Sylvie Putot, editors, Hybrid Systems: Computation and Control (part of CPS Week 2022), HSCC'22. Article No. 2, pp. 1-11. ACM, 2022.
    HSCC Best Paper Award and HSCC Best Repeatability Evaluation Award. © The authors
    [bib | ✂ | pdf | doi | slides | video | kyx | arXiv | artifact]

  3. Brandon Bohrer and André Platzer.
    Structured proofs for adversarial cyber-physical systems.
    ACM Trans. Embed. Comput. Syst. 20(5s), pp. 93:1-93:26, 2021.
    Special issue on EMSOFT 2021. © The authors
    [bib | ✂ | pdf | doi | mypdf | arXiv]

  4. Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
    Pegasus: Sound continuous invariant generation.
    Formal Methods in System Design 58(1), pp. 5-41, 2022.
    Special issue for selected papers from FM'19. © The authors
    [bib | ✂ | pdf | doi | tool | arXiv | FM'19]

  5. 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. 138-157. Springer, 2019. © Springer
    FM Best Tool Paper Award.
    [bib | ✂ | pdf | doi | slides | tool | FMSD]

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

  7. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | ✂ | doi | slides | video | book | web | errata]

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

  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 16-17, 2017, pp. 208-221, ACM, 2017. © ACM
    [bib | ✂ | pdf | doi | slides | Isabelle | Coq]

  10. 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-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015. © Springer
    [bib | ✂ | pdf | doi | slides | poster | tool]

  11. André Platzer.
    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]

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

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

Applications: Techniques & Case Studies

  1. Aditi Kabra, Stefan Mitsch and André Platzer.
    Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces.
    IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), pp. 4409-4420, 2022. Special issue for EMSOFT 2022. © IEEE
    Best paper finalist
    [bib | ✂ | doi | slides | video | kyx | extra]

  2. Rachel Cleveland, Stefan Mitsch and André Platzer.
    Formally verified next-generation airborne collision avoidance games in ACAS X.
    ACM Trans. Embed. Comput. Syst. 22(1), pp. 10:1-10:30, 2023. © The authors
    [bib | ✂ | pdf | doi | mypdf | kyx | arXiv]

  3. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon and André Platzer.
    A formal safety net for waypoint following in ground robots.
    IEEE Robotics and Automation Letters 4(3), pp. 2910-2917, 2019. © IEEE
    [bib | ✂ | pdf | doi | kyx | study | arXiv]

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

  5. 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. 6485-6492. AAAI 2018. © AAAI Press
    [bib | ✂ | pdf | eprint | slides]

  6. Brandon Bohrer, Adriel Luo, Xue An Chuang and André Platzer.
    CoasterX: A case study in component-driven hybrid systems proof automation.
    In Maurice Heemels and Antoine Girard, editors, 6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018, volume 51(6) of IFAC-PapersOnline, pp. 55-60, 2018. © IFAC
    [bib | ✂ | pdf | doi | slides]

  7. 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. 173-191. Springer, 2017. © Springer
    [bib | ✂ | pdf | doi | slides]

  8. 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. 1312-1340, 2017. © The authors
    [bib | ✂ | pdf | doi | kyx | arXiv]

  9. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | ✂ | doi | slides | video | book | web | errata]

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

  11. 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
    [bib | ✂ | pdf | doi | slides | study | STTT'18]

  12. 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 19(6), pp. 717-741, 2017.
    Special issue for selected papers from TACAS'15. © Springer
    [bib | ✂ | pdf | doi | kyx | study | TACAS'15]

  13. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
    A component-based approach to hybrid systems safety verification.
    In Erika Abraham and Marieke Huisman, editors, Integrated Formal Methods - 12th International Conference, iFM 2016, Reykjavik, Iceland, June 1-4, 2016, Proceedings, volume 9681 of LNCS, pp. 441-456. Springer, 2016. © Springer
    [bib | ✂ | pdf | doi | slides | TR]

  14. 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 | mypdf | RV'14]

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

  16. André Platzer.
    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]

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

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.

Copyright © by André Platzer        Last modified: 2023-06-10

Install | Tutorial | Doc | Paper | People | Web