Publications by André Platzer

Table of Contents List of Publications Textbooks Books Book Chapters Journal Publications Conference Publications Short & Tool Publications Workshop Publications Invited Publications Theses Video Productions Reports Other Editor

Publications By Type or By Year or By Area or Guide

List of Publications

[ORCID | DBLP | Google Scholar | by year | by area | abstracts | guide]

Textbooks

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 | abstract]

Books

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 | abstract]

Book Chapters

1. Stefan Mitsch and André Platzer.
   A retrospective on developing hybrid system provers in the KeYmaera family:
      A tale of three provers.
   In Wolfgang Ahrendt et al., editors, Deductive Software Verification: Future Perspectives, volume 12345 of LNCS, pp. 21-64. Springer, 2020. © Springer
   [bib | ⧉ | pdf | doi | abstract]
   
   
2. André Platzer.
   Overview of logical foundations of cyber-physical systems.
   In Helmut Seidl, editor, Post-proceedings of the Summer School Marktoberdorf: Safety and Security of Software Systems - Logics, Proofs, Applications, TUM University Press, 2020. © The author
   [bib | ⧉ | pdf | eprint | arXiv | abstract]
   
   
3. Laurent Doyen, Goran Frehse, George J. Pappas, and André Platzer.
   Verification of hybrid systems.
   In Edmund M. Clarke and Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pp. 1047-1110. Springer, 2018. © Springer
   [bib | ⧉ | pdf | doi | book | abstract]
   
   

Journal Publications

1. Manfred Broy, Achim Brucker, Alessandro Fantechi, Mario Gleirscher, Klaus Havelund, Markus Alexander Kuppe, Alexandra Mendes, André Platzer, Jan Ringert and Allison Sullivan.
   Does every computer scientist need to know formal methods?.
   Form. Asp. Comput. To appear © The authors
   [bib | ⧉ | doi | abstract]
   
   
2. André Platzer.
   Hybrid dynamical systems logic and its refinements.
   Sci. Comput. Program. 239, pp. 103179, 2025. © The authors
   [bib | ⧉ | doi | mypdf | abstract]
   
   
3. 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 | ⧉ | pdf | doi | slides | video | kyx | extra | abstract]
   
   
4. 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 | abstract]
   
   
5. Qin Lin, Stefan Mitsch, André Platzer and John M. Dolan.
   Safe and resilient practical waypoint-following for autonomous vehicles.
   IEEE Control Syst. Lett. 6, pp. 1574-1579, 2022. © IEEE
   [bib | ⧉ | pdf | doi | abstract]
   
   
6. 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 | abstract]
   
   
7. 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 | abstract]
   
   
8. 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 | abstract]
   
   
9. 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 | LICS'18 | abstract]
   
   
10. 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 | abstract]
    
    
11. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
    Tactical contract composition for hybrid system component verification.
    STTT 20(6), pp. 615-643, 2018.
    Special issue for selected papers from FASE'17. © The authors
    [bib | ⧉ | pdf | doi | mypdf | study | FASE'17 | abstract]
    
    
12. 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 | abstract]
    
    
13. 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 | abstract]
    
    
14. André Platzer.
    Differential hybrid games.
    ACM Trans. Comput. Log. 18(3), pp. 19:1-19:44, 2017. © The author
    [bib | ⧉ | pdf | doi | mypdf | arXiv | abstract]
    
    
15. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets.
    Computer Languages, Systems & Structures 47(1), pp. 19-43, 2017.
    Special issue for selected papers from VMCAI'15. © Elsevier
    [bib | ⧉ | pdf | doi | study | VMCAI'15 | abstract]
    
    
16. 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 | abstract]
    
    
17. 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 | abstract]
    
    
18. 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]
    
    
19. 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 | abstract]
    
    
20. Stefan Mitsch, André Platzer, Werner Retschitzegger and Wieland Schwinger.
    Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems.
    ACM Computing Surveys 48(1), pp. 3:1-3:40. 2015. © ACM
    [bib | ⧉ | pdf | doi | abstract]
    
    
21. Khalil Ghorbal, Jean-Baptiste Jeannin, Erik P. Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell.
    Hybrid theorem proving of aerospace systems: Applications and challenges.
    Journal of Aerospace Information Systems 11(10), pp. 702-713. 2014.
    Special issue on Software Challenges in Aerospace. © The authors
    [bib | ⧉ | pdf | doi | abstract]
    
    
22. Akshay Rajhans, Ajinkya Bhave, Ivan Ruchkin, Bruce H. Krogh, David Garlan, André Platzer and Bradley Schmerl.
    Supporting heterogeneity in cyber-physical systems architectures.
    IEEE Transactions on Automatic Control 59(12), pp. 3178-3193, 2014.
    Special issue on Control of Cyber-Physical Systems. © IEEE
    [bib | ⧉ | pdf | doi | abstract]
    
    
23. Stefan Mitsch, Grant Olney Passmore and André Platzer.
    Collaborative verification-driven engineering of hybrid systems.
    Mathematics in Computer Science 8(1), pp. 71-97, 2014.
    Special issue on Enabling Domain Experts to use Formalized Reasoning. © Springer
    [bib | ⧉ | pdf | doi | arXiv | abstract]
    
    
24. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian statistical model checking with application to Simulink/Stateflow verification.
    Formal Methods in System Design 43(2), pp. 338-367, 2013.
    Special issue on Probabilistic Model Checking. © Springer
    [bib | ⧉ | pdf | doi | abstract]
    
    
25. André Platzer.
    A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
    Logical Methods in Computer Science 8(4), pp. 1-44, 2012.
    Special issue for selected papers from CSL'10. © The author
    [bib | ⧉ | pdf | doi | arXiv | CSL'10 | abstract]
    
    
26. 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 | abstract]
    
    
27. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    Formal Methods in System Design 35(1), pp. 98-120, 2009.
    Special issue for selected papers from CAV'08. © Springer
    [bib | ⧉ | pdf | doi | study | CAV'08 | abstract]
    
    
28. 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 | abstract]
    
    
29. 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 | abstract]
    
    

Conference Publications

1. Samuel Teuber, Stefan Mitsch, and André Platzer.
   Provably safe neural network controllers via differential dynamic logic.
   In A. Globerson and L. Mackey and A. Fan and C. Zhang and D. Belgrave and J. Tomczak and U. Paquet, editors, Advances in Neural Information Processing Systems 37 NeurIPS 2024
   [bib | ⧉ | pdf | arXiv | abstract]
   
   
2. Noah Abou El Wafa and André Platzer.
   Complete game logic with sabotage.
   In Pawel Sobocinski, Ugo Dal Lago and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'24, pp. 1:1-1:15, ACM, 2024. © The authors
   [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
   
   
3. Enguerrand Prebet and André Platzer.
   Uniform substitution for differential refinement logic.
   In Christoph Benzmüller, Marijn J. Heule and Renate A. Schmidt, editors, Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Proceedings, volume 14740 of LNCS. pp. 196-215, Springer 2024. © The authors
   [bib | ⧉ | pdf | doi | arXiv | abstract]
   
   
4. Aditi Kabra, Jonathan Laurent, Stefan Mitsch, and André Platzer.
   CESAR: control envelope synthesis via angelic refinements.
   In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, volume 14570 of LNCS, pp. 144-164 Springer, 2024. © The Author(s)
   [bib | ⧉ | pdf | doi | slides | arXiv | artifact | abstract]
   
   
5. 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 | abstract]
   
   
6. Katherine Kosaian, Yong Kiam Tan, and André Platzer.
   A first complete algorithm for real quantifier elimination in Isabelle/HOL.
   CPP 2023, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 211-224. ACM, 2023. © ACM
   [bib | ⧉ | pdf | doi | video | Isabelle | arXiv | abstract]
   
   
7. Jonathan Laurent and André Platzer.
   Learning to find proofs and theorems by learning to refine search strategies:
      The case of loop invariant synthesis.
   In Sanmi Koyejo, Shakir Mohamed, Alekh Agarwal, Danielle Belgrave, Kyunghyun Cho and Alice Oh, editors, Advances in Neural Information Processing Systems 35 NeurIPS 2022 pp. 4843–4856.
   [bib | ⧉ | pdf | eprint | slides | video | poster | arXiv | abstract]
   
   
8. 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 | abstract]
   
   
9. Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer.
   Verified quadratic virtual substitution for real arithmetic.
   In Marieke Huisman, Corina Pasareanu, and Naijun Zhan, editors, FM 2021: Formal Methods, volume 13047 of LNCS, pp. 200-217. Springer, 2021. © Springer
   [bib | ⧉ | pdf | doi | slides | Isabelle | arXiv | abstract]
   
   
10. Katherine Cordwell, Yong Kiam Tan and André Platzer.
    A verified decision procedure for univariate real arithmetic with the BKR algorithm.
    In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29-July 1, 2021, Rome, Italy, volume 193 of LIPIcs, pp. 14:1-14:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021. © The authors
    [bib | ⧉ | pdf | doi | slides | Isabelle | arXiv | abstract]
    
    
11. Yong Kiam Tan and André Platzer.
    Switched systems as hybrid programs.
    In Raphaël M. Jungers, Necmiye Ozay and Alessandro Abate, editors, 7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2021, volume 54(5) of IFAC-PapersOnline, pp. 247-252. 2021. © The authors
    [bib | ⧉ | pdf | doi | kyx | arXiv | abstract]
    
    
12. 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 | abstract]
    
    
13. Brandon Bohrer and André Platzer.
    Refining constructive hybrid games.
    In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29 - July 5, Paris, France, Proceedings, volume 167 of LIPIcs, pp. 14:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv | abstract]
    
    
14. Brandon Bohrer and André Platzer.
    Constructive hybrid games.
    In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, 10th International Joint Conference, IJCAR 2020, Paris, France, Proceedings, Part I, volume 12166 of LNCS, pp. 454-473. Springer 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv | abstract]
    
    
15. Brandon Bohrer and André Platzer.
    Constructive game logic.
    In Peter Müller, editor, Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, volume 12075 of LNCS, pp. 84-111. Springer, 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv | abstract]
    
    
16. João G. Martins, André Platzer, and João Leite.
    Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems.
    In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2019, London, September 3-5, 2019, Proceedings, volume 11714 of LNCS, pp. 428-445. Springer, 2019. © Springer Nature Switzerland AG
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
17. 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'22 | abstract]
    
    
18. 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 | abstract]
    
    
19. 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-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 94-110. Springer, 2019. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
20. Katherine Cordwell and André Platzer.
    Towards physical hybrid systems.
    In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 216-232. Springer, 2019. © Springer
    [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
    
    
21. 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 | errata | abstract]
    
    
22. Nathan Fulton and André Platzer.
    Verifiably safe off-model reinforcement learning.
    In Tomas Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, Proceedings, Part I, volume 11427 of LNCS, pp. 413-430. Springer, 2019. © The authors
    [bib | ⧉ | pdf | doi | arXiv | abstract]
    
    
23. Luis Garcia, Stefan Mitsch and André Platzer.
    HyPLC: Hybrid programmable logic controller program translation for verification.
    In Linda Bushnell and Miroslav Pajic, editors, 10th ACM/IEEE International Conference on Cyber-Physical Systems ICCPS'19, pp. 47-56. 2019. © ACM
    Best paper finalist
    [bib | ⧉ | pdf | doi | tool | arXiv | abstract]
    
    
24. 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 | abstract]
    
    
25. Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André Platzer.
    Vector barrier certificates and comparison systems.
    In Klaus Havelund. Bill Roscoe and Jan Peleska, editors, FM 2018: Formal Methods - 22nd International Symposium, Oxford, UK, July 15-17, 2018, Proceedings, volume 10951 of LNCS, pp. 418-437. Springer, 2018. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
26. Brandon Bohrer and André Platzer.
    A hybrid, dynamic logic for hybrid-dynamic information flow.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 115-124. ACM 2018. © The authors. Publication rights licensed to ACM
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
27. 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 | abstract]
    
    
28. 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 | abstract]
    
    
29. 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 | abstract]
    
    
30. 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 | doi | eprint | slides | abstract]
    
    
31. 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 | abstract]
    
    
32. 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 | abstract]
    
    
33. 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 | abstract]
    
    
34. 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 | abstract]
    
    
35. Sarah M. Loos and André Platzer.
    Differential refinement logic.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, July 5–8, 2016, New York, NY, USA, pp. 505-514. ACM, 2016. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | abstract]
    
    
36. 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 | abstract]
    
    
37. 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 | abstract]
    
    
38. Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson and André Platzer.
    A method for invariant generation for polynomial continuous systems.
    In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, Florida, USA, January 17-19, 2016, Proceedings, volume 9583 of LNCS, pp. 268-288. Springer, 2016. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
39. Andreas Müller and Stefan Mitsch and André Platzer.
    Verified traffic networks: Component-based verification of cyber-physical flow systems.
    In Intelligent Transportation Systems ITSC'15', IEEE 18th International Conference on, pp. 757-764, 2015. © IEEE
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
40. Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, and Bruce Krogh.
    Forward invariant cuts to simplify proofs of safety.
    In Alain Girault and Nan Guan, editors, International Conference on Embedded Software, EMSOFT'15, Amsterdam, The Netherlands, Proceedings, pp. 227-236. IEEE, 2015. © IEEE
    [bib | ⧉ | pdf | doi | arXiv | abstract]
    
    
41. 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 | abstract]
    
    
42. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
    A formally verified hybrid system for the next-generation airborne collision avoidance system.
    In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, London, UK, April 11-18, 2015, Proceedings, volume 9035 of LNCS, pp. 21-36. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | study | TR | STTT'17 | abstract]
    
    
43. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    A hierarchy of proof rules for checking differential invariance of algebraic sets.
    In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015, Proceedings, volume 8931 of LNCS, pp. 431-448. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | slides | study | ComLan'17 | abstract]
    
    
44. 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 | abstract]
    
    
45. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    Invariance of conjunctions of polynomial equalities for algebraic differential equations.
    In Markus Müller-Olm and Helmut Seidl, editors, 21st International Static Analysis Symposium, SAS 2014, volume 8723 of LNCS, pp. 151-167. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
46. Jean-Baptiste Jeannin and André Platzer.
    dTL²: Differential temporal dynamic logic with nested temporalities for hybrid systems.
    In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, Automated Reasoning, 7th International Joint Conference, IJCAR 2014, Vienna, Austria, July 19-22, 2014, Proceedings, volume 8562 of LNCS, pp. 292-306. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
47. Stefan Mitsch, Jan-David Quesel and André Platzer.
    Refactoring, refinement, and reasoning:
       A logical characterization for hybrid systems.
    In Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, editors, 19th International Symposium on Formal Methods, FM'14, Singapore, Proceedings, volume 8442 of LNCS, pp. 481-496. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
48. Khalil Ghorbal and André Platzer.
    Characterizing algebraic invariants by differential radical invariants.
    In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pp. 279-294. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | abstract]
    
    
49. Sarah M. Loos, David Witmer, Peter Steenkiste and André Platzer.
    Efficiency analysis of formally verified adaptive cruise controllers.
    In Andreas Hegyi and Bart De Schutter, editors, 16th International IEEE Conference on Intelligent Transportation Systems, ITSC'13, The Hague, Netherlands, Proceedings, 2013. © IEEE
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
50. Stefan Mitsch, Khalil Ghorbal and André Platzer.
    On provably safe obstacle avoidance for autonomous robotic ground vehicles.
    In Paul Newman, Dieter Fox, and David Hsu, editors, Robotics: Science and Systems, RSS 2013. © The author
    [bib | ⧉ | pdf | eprint | slides | video | study | IJRR'17 | abstract]
    
    
51. Erik P. Zawadzki, André Platzer and Geoffrey J. Gordon.
    A generalization of SAT and #SAT for policy evaluation.
    In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23nd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pp. 2583-2589, IJCAI/AAAI, 2013.
    [bib | ⧉ | pdf | eprint | poster | TR | abstract]
    
    
52. Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
    Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 263-272. ACM, 2013. © ACM
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
53. Sarah M. Loos, David W. Renshaw and André Platzer.
    Formal verification of distributed aircraft controllers.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 125-130. ACM, 2013. © ACM
    [bib | ⧉ | pdf | doi | slides | poster | study | TR | abstract]
    
    
54. David Henriques, João G. Martins, Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Statistical model checking for Markov decision processes.
    In 9th International Conference on Quantitative Evaluation of Systems, QEST 2012, September 17-20, London, UK, pp. 84-93. IEEE Computer Society, 2012. © IEEE
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
55. Jan-David Quesel and André Platzer.
    Playing hybrid games with KeYmaera.
    In Bernhard Gramlich, Dale Miller and Ulrike Sattler, editors, Automated Reasoning, 6th International Joint Conference, IJCAR'12, Manchester, UK, Proceedings, volume 7364 of LNCS, pp. 439-453. Springer, 2012. © Springer
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
56. 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 | abstract]
    
    
57. Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
    Using theorem provers to guarantee closed-loop system properties.
    In Dawn Tilbury, editor, American Control Conference, ACC'12, Montréal, Canada, June 27-29. pp. 3573-3580. 2012. © IEEE
    [bib | ⧉ | pdf | doi | abstract]
    
    
58. Stefan Mitsch, Sarah M. Loos and André Platzer.
    Towards formal verification of freeway traffic control.
    In Chenyang Lu, editor, ACM/IEEE Third International Conference on Cyber-Physical Systems ICCPS'12, Beijing, China, April 17-19. pp. 171-180, IEEE. 2012. © IEEE
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
59. Akshay Rajhans, Ajinkya Bhave, Sarah M. Loos, Bruce H. Krogh, André Platzer and David Garlan.
    Using parameters in architectural views to support heterogeneous design and verification.
    In 50th IEEE Conference on Decision and Control and European Control Conference CDC'11. pp. 2705-2710, IEEE. 2011. © IEEE
    [bib | ⧉ | pdf | doi | TAC'14 | abstract]
    
    
60. Sarah M. Loos and André Platzer.
    Safe intersections: At the crossing of hybrid systems and verification.
    In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 1181-1186. 2011. © IEEE
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
61. João G. Martins, André Platzer and João Leite.
    Statistical model checking for distributed probabilistic control hybrid automata with smart grid applications.
    In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pp. 131-146. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
62. David W. Renshaw, Sarah M. Loos and André Platzer.
    Distributed theorem proving for distributed hybrid systems.
    In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pp. 356-371. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | tool | study | errata | abstract]
    
    
63. André Platzer.
    Stochastic differential dynamic logic for stochastic hybrid programs.
    In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, International Conference on Automated Deduction, CADE-23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446-460. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
64. Sicun Gao, André Platzer and Edmund M. Clarke.
    Quantifier elimination over finite fields with Gröbner bases.
    In Franz Winkler, editor, Algebraic Informatics, Fourth International Conference, CAI 2011, Linz, Austria, June 21-24, 2011, Proceedings, volume 6742 of LNCS, pp. 140-157. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | arXiv | abstract]
    
    
65. Sarah M. Loos, André Platzer and Ligia Nistor.
    Adaptive cruise control:
       Hybrid, distributed, and now formally verified.
    In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 42-56. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | abstract]
    
    
66. Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer.
    An Instantiation-Based Theorem Prover for First-Order Programming.
    In 14th International Conference on Artificial Intelligence and Statistics (AISTATS) 2011, Fort Lauderdale, FL, USA, Proceedings, volume 15 of JMLR W&CP, pp. 855-863, 2011.
    [bib | ⧉ | pdf | poster | proceedings | abstract]
    
    
67. André Platzer.
    Quantified differential invariants.
    In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, pp. 63-72. ACM, 2011. © ACM
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
68. André Platzer.
    Quantified differential dynamic logic for distributed hybrid systems.
    In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pp. 469-483. Springer, 2010. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | LMCS'12 | abstract]
    
    
69. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian statistical model checking with application to Simulink/Stateflow verification.
    In Karl Henrik Johansson and Wang Yi, editors, Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, pp. 243-252. ACM, 2010. © ACM
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
70. André Platzer and Jan-David Quesel.
    European Train Control System: A case study in formal verification.
    In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM'09, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pp. 246-265. Springer, 2009. © Springer
    [bib | ⧉ | pdf | doi | slides | kyx | TR | old | abstract]
    
    
71. André Platzer and Edmund M. Clarke.
    Formal verification of curved flight collision avoidance maneuvers: A case study.
    In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pp. 547-562. Springer, 2009. © Springer
    FM Best Paper Award.
    [bib | ⧉ | pdf | doi | slides | study | TR | abstract]
    
    
72. Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
    A Bayesian approach to model checking biological systems.
    In Pierpaolo Degano and Roberto Gorrieri, editors, Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, Proceedings, volume 5688 of LNCS, pp. 218-234. Springer, 2009. © Springer
    [bib | ⧉ | pdf | doi | TR | abstract]
    
    
73. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real world verification.
    In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE-22, Montreal, Canada, Proceedings, volume 5663 of LNCS, pp. 485-501. Springer, 2009. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | smtlib | abstract]
    Introduces a decision procedure for universal nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the Real Nullstellensatz.
    
    
74. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pp. 176-189, Springer, 2008. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | FMSD'09 | abstract]
    
    
75. 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 | abstract]
    
    
76. André Platzer.
    A temporal dynamic logic for verifying hybrid system invariants.
    In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pp. 457-471. Springer, 2007. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | abstract]
    
    
77. André Platzer and Edmund M. Clarke.
    The image computation problem in hybrid systems model checking.
    In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 473-486. Springer, 2007, © Springer
    [bib | ⧉ | pdf | doi | slides | tool | abstract]
    
    
78. Bernhard Beckert and André Platzer.
    Dynamic logic with non-rigid functions:
       A basis for object-oriented program verification.
    In Uli Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS, pp. 266-280. Springer, 2006. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    

Short & Tool Publications

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 | abstract]
   
   
2. 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 | tooldoi | abstract]
   
   
3. 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]
   
   
4. André Platzer and Jan-David Quesel.
   Logical verification and systematic parametric analysis in train control.
   In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pp. 646-649. Springer, 2008. © Springer
   [bib | ⧉ | pdf | doi | poster | abstract]
   
   
5. André Platzer.
   Differential logic for reasoning about hybrid systems.
   In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 746-749. Springer, 2007. © Springer
   [bib | ⧉ | pdf | doi | poster | abstract]
   
   

Workshop Publications

1. Andreas Müller, Stefan Mitsch, Wieland Schwinger and André Platzer.
   A component-based hybrid systems verification and implementation tool in KeYmaera X.
   In Roger Chamberlain, Walid Taha and Martin Törngren, editors, CyPhy 2018, WESE 2018: Cyber Physical Systems. Model-Based Design, revised selected papers, volume 11615 of LNCS, pp. 91-110. Springer, 2019. © Springer
   [bib | ⧉ | pdf | doi | abstract]
   
   
2. Stefan Mitsch and André Platzer.
   The KeYmaera X proof IDE:
      Concepts on usability in hybrid systems theorem proving.
   In Catherine Dubois, Paolo Masci and Dominique Méry, editors, 3rd Workshop on Formal Integrated Development Environment F-IDE 2016, volume 240 of EPTCS, pp. 67-81, 2017. © The authors
   [bib | ⧉ | pdf | doi | tool | arXiv | abstract]
   
   
3. Stefan Mitsch, Jan-David Quesel, and André Platzer.
   From safety to guilty & from liveness to niceness.
   In Calin Belta and Hadas Kress-Gazit, editors, 5th Workshop on Formal Methods for Robotics and Automation, 2014. © The author
   [bib | ⧉ | pdf | abstract]
   
   
4. Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer .
   A projection algorithm for strictly monotone linear complementarity problems.
   In 6th NIPS Workshop on Optimization for Machine Learning, 2013.
   [bib | ⧉ | pdf | eprint | abstract]
   
   
5. André Platzer.
   Teaching CPS foundations with contracts.
   First Workshop on Cyber-Physical Systems Education (CPS-Ed 2013), pp. 7-10. 2013.
   [bib | ⧉ | pdf | eprint | slides | poster | course | abstract]
   
   
6. André Platzer.
   Combining deduction and algebraic constraints for hybrid system analysis.
   In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
   [bib | ⧉ | pdf | eprint | slides | abstract]
   
   
7. Stephanie Kemper and André Platzer.
   SAT-based abstraction refinement for real-time systems.
   In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, Electr. Notes Theor. Comput. Sci., 182:107-122, 2007
   [bib | ⧉ | pdf | doi | slides | tool | abstract]
   
   
8. André Platzer.
   Towards a hybrid dynamic logic for hybrid dynamic systems.
   In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva and Jørgen Villadsen, editors, Proc., International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, Electr. Notes Theor. Comput. Sci. 174(6):63-77, 2007.
   [bib | ⧉ | pdf | doi | slides | abstract]
   
   

Invited Publications

1. André Platzer.
   Intersymbolic AI:
      Interlinking symbolic AI and subsymbolic AI.
   In Tiziana Margaria and Bernhard Steffen, editors, ISoLA 2024, Proceedings, volume 15222 of LNCS, pp. 162-180. Springer 2024. © The Author(s), under exclusive license to Springer Nature
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
   
   
2. André Platzer.
   The significance of symbolic logic for scientific education.
   In Emil Sekerinski and Leila Ribeiro, editors, Formal Methods Teaching: 6th International Workshop, FMTea 2024, Proceedings, volume 14939 of LNCS, pp. 3-22. Springer 2024. © The Author(s)
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
   
   
3. André Platzer.
   Refinements of hybrid dynamical systems logic.
   In Uwe Glässer, José Creissac Campos, Dominique Méry, Philippe Palanque, editors, Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, Proceedings. volume 14010 of LNCS. pp 3-14. Springer, 2023. © The author under exclusive license to Springer Nature
   Invited paper.
   [bib | ⧉ | doi | slides | SCP'25 | abstract]
   
   
4. André Platzer.
   Overview of logical foundations of cyber-physical systems.
   In Helmut Seidl, editor, Post-proceedings of the Summer School Marktoberdorf: Safety and Security of Software Systems - Logics, Proofs, Applications, TUM University Press, 2020. © The author
   [bib | ⧉ | pdf | eprint | arXiv | abstract]
   
   
5. André Platzer.
   The logical path to autonomous cyber-physical systems.
   In David Parker and Verena Wolf, editors, International Conference on Quantitative Evaluation of SysTems, QEST 2019, Glasgow, UK, Proceedings, volume 11785 of LNCS, pp. 25-33. Springer, 2019. © Springer
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | abstract]
   
   
6. Nathan Fulton and André Platzer.
   Safe AI for CPS.
   In International Testing Conference ITC'18, IEEE, 2018. © IEEE
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | abstract]
   
   
7. Franz Franchetti, Tze Meng Low, Stefan Mitsch, Juan Paolo Mendoza, Liangyan Gui, Amarin Phaosawasdi, David Padua, Soummya Kar, José M. F. Moura, Mike Franusich, Jeremy Johnson, André Platzer and Manuela Veloso.
   High-assurance SPIRAL:
      End-to-end guarantees for robot and car control.
   IEEE Control Systems 37(2), pp. 82-103. 2017. © IEEE
   [bib | ⧉ | pdf | doi]
   
   
8. 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
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | abstract]
   
   
9. André Platzer.
   How to prove hybrid systems and why that matters.
   International Conference on Complex Systems Engineering, ICCSE 2015 © IEEE
   Invited paper
   [bib | ⧉ | pdf | doi | abstract]
   
   
10. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
    Formal verification of ACAS X, an industrial airborne collision avoidance system.
    In Alain Girault and Nan Guan, editors, International Conference on Embedded Software, EMSOFT'15, Amsterdam, The Netherlands, Proceedings, pp. 127-136. IEEE Press, 2015. © IEEE
    [bib | ⧉ | pdf | doi | abstract]
    
    
11. André Platzer.
    Analog and hybrid computation: Dynamical systems and programming languages.
    Bulletin of the EATCS 114, 2014. © The author
    Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
    [bib | ⧉ | pdf | eprint | abstract]
    
    
12. André Platzer.
    Logical analysis of hybrid systems:
       A complete answer to a complexity challenge.
    Journal of Automata, Languages and Combinatorics 17(2-4), pp. 265-275. 2012.
    Invited Paper
    [bib | ⧉ | pdf | doi | abstract]
    
    
13. André Platzer.
    Logical analysis of hybrid systems:
       A complete answer to a complexity challenge.
    In Martin Kutrib, Nelma Moreira and Rogério Reis, editors, Descriptional Complexity of Formal Systems, DCFS'12, Braga, Portugal, Proceedings, volume 7386 of LNCS, pp. 43-49. Springer, 2012. © Springer
    Invited Paper
    [bib | ⧉ | pdf | doi | abstract]
    
    
14. André Platzer.
    A differential operator approach to equational differential invariants.
    In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pp. 28-48. Springer, 2012. © Springer
    Invited paper.
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
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 | abstract]
    
    
16. Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
    Using theorem provers to guarantee closed-loop system properties.
    In Dawn Tilbury, editor, American Control Conference, ACC'12, Montréal, Canada, June 27-29. pp. 3573-3580. 2012. © IEEE
    [bib | ⧉ | pdf | doi | abstract]
    
    
17. Sarah M. Loos and André Platzer.
    Safe intersections: At the crossing of hybrid systems and verification.
    In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 1181-1186. 2011. © IEEE
    [bib | ⧉ | pdf | doi | slides | study | abstract]
    
    
18. 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
    Invited tutorial.
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
19. André Platzer.
    Differential dynamic logic:
       Automated theorem proving for hybrid systems.
    Künstliche Intelligenz 24(1), pp. 75-77, 2010. © Springer
    Invited paper.
    [bib | ⧉ | doi | abstract]
    
    
20. André Platzer.
    Verification of cyberphysical transportation systems.
    IEEE Intelligent Systems 24(4), pp. 10-13, Jul/Aug, 2009. © IEEE
    Invited paper.
    [bib | ⧉ | doi | abstract]
    
    
21. Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken and Boris Wirtz.
    Automating verification of cooperation, control, and design in traffic applications.
    In Cliff Jones, Zhiming Liu and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pp. 115-169. Springer, 2007. © Springer
    Invited paper.
    [bib | ⧉ | pdf | doi | abstract]
    
    

Theses

1. 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 | abstract]
   
   
2. André Platzer.
   An Object-oriented Dynamic Logic with Updates.
   Master's Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, September 2004.
   Short version appeared as Dynamic logic with non-rigid functions: A basis for object-oriented program verification at IJCAR 2006.
   [bib | ⧉ | pdf | slides | IJCAR'06 | abstract]
   
   
3. André Platzer.
   Using a Program Verification Calculus for Constructing Specifications from Implementations.
   Minor Thesis (Studienarbeit), University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, February 2004.
   [bib | ⧉ | pdf | slides | abstract]
   
   

Video Productions

1. André Platzer.
   Videos for Logical Foundations of Cyber-Physical Systems.
   YouTube 2018-2019. Videos for 22 lectures of about an hour each.
   [bib | ⧉ | video | Textbook | abstract]
   
   

Reports

[arXiv]

1. Brandon Bohrer, Manuel Fernández and André Platzer.
   dL_ɩ: Definite Descriptions in Differential Dynamic Logic.
   School of Computer Science, Carnegie Mellon University, CMU-CS-19-111, 2019.
   [bib | ⧉ | pdf | CADE]
   
   
2. Brandon Bohrer and André Platzer.
   A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.
   School of Computer Science, Carnegie Mellon University, CMU-CS-18-105, 2018.
   [bib | ⧉ | pdf | LICS'18]
   
   
3. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
   A Component-based Approach to Hybrid Systems Safety Verification.
   School of Computer Science, Carnegie Mellon University, CMU-CS-16-100, 2016.
   [bib | ⧉ | pdf | IFM'16]
   
   
4. André Platzer and Yong Kiam Tan.
   How to Prove "All" Differential Equation Properties.
   School of Computer Science, Carnegie Mellon University, CMU-CS-17-117, 2017. Extended version arXiv:1802.01226
   [bib | ⧉ | pdf | arXiv | LICS'18]
   
   
5. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
   A Component-based Approach to Hybrid Systems Safety Verification.
   School of Computer Science, Carnegie Mellon University, CMU-CS-16-100, 2016.
   [bib | ⧉ | pdf | IFM'16]
   
   
6. André Platzer.
   Differential Hybrid Games.
   School of Computer Science, Carnegie Mellon University, CMU-CS-14-102, December 2014. Extended version arXiv:1507.04943.
   [bib | ⧉ | pdf | arXiv | TOCL'17 | abstract]
   
   
7. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
   A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System.
   School of Computer Science, Carnegie Mellon University, CMU-CS-14-138, 2014.
   [bib | ⧉ | pdf | study | TACAS'15 | abstract]
   
   
8. Stefan Mitsch and André Platzer.
   ModelPlex: Verified Runtime Validation of Verified Cyber-physical System Models.
   School of Computer Science, Carnegie Mellon University, CMU-CS-14-121, 2014.
   [bib | ⧉ | pdf | study | RV'14 | abstract]
   
   
9. Khalil Ghorbal and André Platzer.
   Characterizing Algebraic Invariants by Differential Radical Invariants.
   School of Computer Science, Carnegie Mellon University, CMU-CS-13-129, 2013.
   [bib | ⧉ | pdf | TACAS'14 | abstract]
   
   
10. Erik Zawadzki, André Platzer, and Geoffrey J. Gordon.
    A Generalization of SAT and #SAT for Robust Policy Evaluation.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-107, 2013.
    [bib | ⧉ | pdf | IJCAI'13 | abstract]
    
    
11. Yanni Kouskoulas, André Platzer and Peter Kazanzides.
    Formal Methods for Robotic System Control Software.
    Johns Hopkins APL Technical Digest 32(2), pp. 490-498, 2013.
    [bib | ⧉ | pdf | abstract]
    
    
12. André Platzer.
    A Complete Axiomatization of Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-100R, January 2013, extended in revised version from July 2013. Extended version arXiv:1408.1980.
    [bib | ⧉ | pdf | slides | arXiv | TOCL'15 | abstract]
    
    
13. David Renshaw, Sarah M. Loos and André Platzer.
    Mechanized Safety Proofs for Disc-Constrained Aircraft.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-132, August 2012.
    [bib | ⧉ | pdf | HSCC'13 | abstract]
    
    
14. André Platzer.
    Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-105, March 2012.
    Also see new results.
    [bib | ⧉ | pdf | TOCL'15 | abstract]
    
    
15. André Platzer.
    The Complete Proof Theory of Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-144, November 2011.
    [bib | ⧉ | pdf | LICS'12]
    
    
16. David W. Renshaw and André Platzer.
    Differential Invariants and Symbolic Integration for Distributed Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-107, May 2012.
    [bib | ⧉ | pdf]
    
    
17. André Platzer.
    The Structure of Differential Invariants and Differential Cut Elimination.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-112, April 2011.
    [bib | ⧉ | pdf | arXiv | LMCS'12]
    
    
18. André Platzer.
    Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-111, 2011.
    [bib | ⧉ | pdf | CADE]
    
    
19. Sarah M. Loos, André Platzer and Ligia Nistor.
    Adaptive Cruise Control:
       Hybrid, Distributed, and Now Formally Verified.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-107, 2011.
    [bib | ⧉ | pdf | FM'10]
    
    
20. André Platzer.
    Quantified Differential Dynamic Logic for Distributed Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-10-126, 2010.
    [bib | ⧉ | pdf | CSL'10]
    
    
21. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian Statistical Model Checking with Application to Simulink/Stateflow Verification.
    School of Computer Science, Carnegie Mellon University, CMU-CS-10-100, 2010.
    [bib | ⧉ | pdf | HSCC'10]
    
    
22. André Platzer and Jan-David Quesel.
    European Train Control System: A Case Study in Formal Verification.
    Reports of SFB/TR 14 AVACS 54, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | ⧉ | pdf | ICFEM'09]
    
    
23. André Platzer and Edmund M. Clarke.
    Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
    School of Computer Science, Carnegie Mellon University, CMU-CS-09-147, 2009.
    [bib | ⧉ | pdf | FM'09]
    
    
24. Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
    A Bayesian Approach to Model Checking Biological Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-09-110, 2009.
    [bib | ⧉ | pdf | CMSB'09]
    
    
25. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real World Verification.
    Reports of SFB/TR 14 AVACS 52, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | ⧉ | pdf | CADE]
    
    
26. André Platzer and Edmund M. Clarke.
    Computing Differential Invariants of Hybrid Systems as Fixedpoints.
    School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
    [bib | ⧉ | pdf | CAV'08]
    
    
27. André Platzer.
    Differential Dynamic Logic for Verifying Parametric Hybrid Systems.
    Reports of SFB/TR 14 AVACS 15, May 2007. ISSN: 1860-9821, www.avacs.org.
    [bib | ⧉ | pdf | TABLEAUX'07]
    
    
28. André Platzer.
    A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
    Reports of SFB/TR 14 AVACS 12, February 2007. ISSN: 1860-9821, www.avacs.org.
    [bib | ⧉ | pdf | LFCS'07]
    
    

Other

1. André Platzer and Long Qian.
   Axiomatization of compact initial value problems: Open properties.
   arXiv:2410.13836, October 2024.
   [bib | ⧉ | pdf | arXiv]
   
   
2. William Simmons and André Platzer.
   Differential elimination and algebraic invariants of polynomial dynamical systems.
   arXiv:2301.10935, January 2023.
   [bib | ⧉ | pdf | arXiv]
   
   
3. Noah Abou El Wafa and André Platzer.
   First-order game logic and modal mu-calculus.
   arXiv:2201.10012, January 2022.
   [bib | ⧉ | pdf | arXiv]
   
   
4. André Platzer.
   KeYmaera X Tutorial.
   66 pages. Fall 2019 © The author
   [bib | ⧉ | pdf | www]
   
   
5. Stefan Mitsch and André Platzer.
   Verified runtime validation for partially observable hybrid systems.
   arXiv:1811.06502, November 2018.
   [bib | ⧉ | pdf | arXiv | abstract]
   
   
6. Sarah M. Loos and André Platzer.
   Teaching cyber-physical systems with logic.
   Draft, 2014.
   [bib | ⧉ | pdf | course | abstract]
   
   
7. André Platzer.
   Dynamic logics of dynamical systems.
   arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
   [bib | ⧉ | pdf | arXiv | LICS'12 | abstract]
   
   

Editor

1. André Platzer and Geoff Sutcliffe.
   Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings.
   volume 12699 of LNCS. Springer, 2021. © The editor(s) and the author(s)
   [bib | ⧉ | doi]
   
   
2. Roland Meyer, André Platzer, and Heike Wehrheim.
   Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings.
   volume 9360 of LNCS. Springer, 2015. © Springer
   [bib | ⧉ | doi]
   
   

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.