André Platzer @ Carnegie Mellon University

André Platzer
André Platzer 0000-0001-7238-5710ORCID iD icon Curriculum Vitae
Professor Email:
Computer Science Department Phone: +1 (412) 268-1558
Carnegie Mellon University Fax: +1 (412) 268-5576
Pittsburgh, PA 15213-3891, USA      Office: GHC 9103
Research interests:
Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Theorem Proving, Formal Methods


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]

Brief Introduction to Logical Foundations of Cyber-Physical Systems (10min)

[Brief (10min) | Overview (40min) | More Videos]

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid SystemsLogical Foundations of Cyber-Physical Systems
Differential equation invariance axiomatization (J.ACM)15-424: Logical Foundations of Cyber-Physical Systems (Fa'21)
Logic for Hybrid GamesLogical Foundations of Cyber-Physical Systems
Formal verification of obstacle avoidance and navigation of ground robots (IJRR'17)A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system (STTT'17)
Logic for Distributed Hybrid SystemsCase Study: Formal Verification of Curved Flight Collision Avoidance Maneuvers
KeYmaera: A Hybrid Theorem Prover for Hybrid SystemsLogical Analysis of Hybrid Systems

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.


More: Read about this research in the news.