André Platzer is a Professor of Computer Science 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 | manifesto | survey | videos | research]
Profile
André Platzer  0000-0001-7238-5710 | Curriculum Vitae | |
| Professor | Email: | ude.umc.sc@reztalpa |
| Computer Science Department | Phone: | +1 (412) 268-1558 |
| Carnegie Mellon University | Office: | GHC 9103 |
| Pittsburgh, PA 15213-3891, USA | Place: | Gates-Hillman Center |
- Research interests:
- Logic of Dynamical Systems, Logic of Autonomous Dynamical Systems, Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Theorem Proving, Formal Methods
[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).
Announcements
- I'm looking for PhD students / postdocs.
- CADE-28: The 28th International Conference on Automated Deduction went Open Access
- 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