André Platzer is the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology and is the founder of the Logical Systems Lab at Carnegie Mellon University. He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. Prof. Platzer pursues this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees. [ textbook | mission | survey | videos | research ]
Profile
| André Platzer | |||||
| Alexander von Humboldt Professor |  0000-0001-7238-5710 |
||||
| KIT Department of Informatics | Email: | ude.tik@reztalp | |||
| Karlsruhe Institute of Technology | Office: | Building 50.34, Room 155 | |||
| Am Fasanengarten 5 | Hours: | by appointment | |||
| 76131 Karlsruhe, Germany | Assistant: | laurence.boehnke@kit.edu | |||
- Research interests:
- Logic of Dynamical Systems, Logic of Autonomous Dynamical Systems, Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Theorem Proving, Formal Methods
[AvH Video (2min) | Brief Video (10min) | Overview Video (40min) | More Videos ]
Topics
 |  |
 |  |
 |  |
 |  |
 |  |
 |  |
The KeYmaera X aXiomatic Theorem Prover for Hybrid Systems is a verification tool. It is based on differential dynamic logic, which provides the Logical Foundations of Cyber-Physical Systems as explained in a recent textbook.
If you want to do research with me, you should take the Logical Foundations of Cyber-Physical Systems course, read the textbook and/or watch the video lectures.
My publications are available in the List of Publications (also see Reading Guide).
Logics
Many of the research findings in my group are rooted in logic, most notably Differential Dynamic Logic for hybrid systems and Differential Game Logic for hybrid games, but also Differential Refinement Logic for proving and using relationships among hybrid systems as well as Stochastic Differential Dynamic Logic for stochastic hybrid systems. [ dL | dGL | overview]
 | |
 |  |
Announcements
- Open PhD Doctoral Researcher / PhD Student Positions at KIT: Alexander von Humboldt Professor group and DFG SFB Sonderforschungsbereich Convide and KiKIT Kerninformatik [AvH | SFB | KiKIT]
- Dr. Katherine Kosaian received the Bill McCune PhD Award in Automated Reasoning 2024 [CMU news | KIT news]
- Attend Formal Methods 2024 and check out the new FM Tutorial Papers and Open Access proceedings Part I and Part II
- KiKIT Kerninformatik -- core informatics research at KIT Helmholtz
- Final round of Bundeswettbewerb Informatik 2023 is at KIT [results]
- DFG SFB 1608 Convide: Consistency in the View-Based Development of Cyber-Physical Systems
- Alexander von Humboldt Professorship for AI at KIT [news | award ceremony]
- Let me know what you think of my suggestion of how to define or recognize a digital twin.
Turing's Twin Test: If a person who can interact with a system and its digital twin by making observations cannot tell the system and its twin apart, then the twin passed Turing's Twin Test. The notion of permitted observations typically limits the permitted questions/properties. - Dr. Yong Kiam Tan received the CMU School of Computer Science Distinguished Dissertation Award 2022
- New course on Logical Foundations of Cyber-Physical Systems at KIT
- Alexander von Humboldt Professorship for AI 2023: KIT, CMU.
- CADE-28: The 28th International Conference on Automated Deduction went Open Access
- Dr. Rose Bohrer received a CMU School of Computer Science Distinguished Dissertation Honorable Mention Award 2021
- KeYmaera X Tutorial on hybrid systems modeling and proving
- Video lectures on Logical Foundations of Cyber-Physical Systems for the textbook
- Textbook on Logical Foundations of Cyber-Physical Systems 2018
- Lectures at Marktoberdorf Summer School 2019
- Dr. Sarah Loos received a CMU School of Computer Science Distinguished Dissertation Honorable Mention Award 2016