André Platzer @ Carnegie Mellon University

André Platzer @ Carnegie Mellon University
André Platzer Curriculum Vitae
Associate Professor Email: send 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]

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems15-424: Foundations of Cyber-Physical Systems (Sp'17)
Logic for Hybrid GamesLogical Foundations of Cyber-Physical Systems
KeYmaera: A Hybrid Theorem Prover for Hybrid SystemsLogical Analysis of Hybrid Systems
Logic for Distributed Hybrid SystemsA formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system
Differential Radical InvariantsCase Study: Formal Verification of Curved Flight Collision Avoidance Maneuvers
Case Study: European Train Control System

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 in the Teaching Section. My personal web pages CMU Web Page and are mirrors.

Publications are available at the List of Publications.


More: Read about this research in the news.