André Platzer @ Carnegie Mellon University

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

The KeYmaera X aXiomatic Theorem Prover for Hybrid Systems is a practical verification tool. The family of differential dynamic logics for hybrid systems verification that it implements are explained as well as more general Logical Foundations of Cyber-Physical Systems.

Information on the courses I teach at Carnegie Mellon University are under Teaching. If you want to do research with me, you should take the Logical Foundations of Cyber-Physical Systems course.

Publications are available at the List of Publications.

Announcements

• FM 2019 Tutorial on KeYmaera X: Modular Formal Verification of Cyber-Physical Systems with KeYmaera X
• Upcoming lectures at Marktoberdorf Summer School 2019
• Video lectures on Logical Foundations of Cyber-Physical Systems for the textbook
• POPL 2019 Tutorial on Programming Cyber-Physical Systems With Logic
• We're looking for Postdocs and PhD students for a new project. PhD applications are via the Computer Science Department at Carnegie Mellon University
• Hot off the press: textbook on Logical Foundations of Cyber-Physical Systems 2018
• Lectures at Marktoberdorf Summer School 2017