André Platzer is an Assistant Professor of Computer Science at Carnegie Mellon University. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes. He received an M.Sc. from the University of Karlsruhe (TH), Germany, in 2004 and a Ph.D. in Computer Science from the University of Oldenburg, Germany, in 2008, after which he joined CMU as an Assistant Professor.
Dr. Platzer received a number of awards for his research on logic of dynamical systems, cyber-physical systems, programming languages, and theorem proving, including an NSF CAREER Award and ACM Doctoral Dissertation Honoroable Mention Award. He was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI’s 10 to Watch by the IEEE Intelligent Systems magazine.
Highlights of Platzer’s thoughts, from the interview below:
- KeYmaera is a formal verification tool for cyber-physical systems. It has seen many real-world applications, e.g. verifying non-collision in the European Train Control System.
- KeYmaera’s capability comes from Platzer’s “differential dynamic logic,” which builds on earlier work in (e.g.) dynamic logic.
- Contra Levitt, Platzer isn’t convinced that autonomous robots will need to use decision theory, though they may.
- Platzer contrasts formal verification (“did I build the system right?”) with formal validation (“did I build the right system?”). One way to make progress on the latter is to develop what Rushby called “deep assumption tracking.”