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 in Computer Science, Cyber-Physical Systems, Programming Languages, Theorem Proving, Formal Methods
Overview
My research develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to show how we can design systems that are guaranteed to interact correctly with the physical world. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. I pursue this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees. [details]
[Brief (10min) | Overview (40min) | More Videos]
Topics
 |  |
 |  |
 |  |
 |  |
 |  |
 |  |
The KeYmaera X aXiomatic Theorem Prover for Hybrid Systems is a verification tool. It is based on the family of differential dynamic logics, which develop the Logical Foundations of Cyber-Physical Systems explained in a recent textbook.
If you want to do research with me, you should take the Logical Foundations of Cyber-Physical Systems course.
Publications are available in the List of Publications.
Announcements
- CADE-28: The 28th International Conference on Automated Deduction went Open Access
- I'm looking for PhD students. PhD applications are central via the Computer Science Department at Carnegie Mellon University
- KeYmaera X Tutorial
- Video lectures on Logical Foundations of Cyber-Physical Systems for the textbook
- Textbook on Logical Foundations of Cyber-Physical Systems 2018