André Platzer @ Karlsruhe Institute of Technology || Carnegie Mellon University

  1. Home

André Platzer is the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology and a Professor of Computer Science at Carnegie Mellon University. He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. Prof. Platzer pursues this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees. [textbook | mission | survey | videos | research]

Profile

André Platzer
André Platzer ORCID iD icon0000-0001-7238-5710
Alexander von Humboldt Professor     Professor of Computer Science
KIT Department of Informatics Computer Science Department
Karlsruhe Institute of Technology Carnegie Mellon University
Am Fasanengarten 5 5000 Forbes Avenue
76131 Karlsruhe, Germany      Pittsburgh, PA 15213-3891, USA     
Email: ude.tik@reztalp Email: ude.umc.sc@reztalpa
Office: Building 50.34 Office: GHC 9103
Phone: +49 721 608-43391 Phone: +1 412 268-1558
Research interests:
Logic of Dynamical Systems, Logic of Autonomous Dynamical Systems, Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Theorem Proving, Formal Methods
Brief Introduction to Logical Foundations of Cyber-Physical Systems (10min)

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


Topics

KeYmaera X Software: An aXiomatic Tactical Theorem Prover for Hybrid SystemsTextbook: Logical Foundations of Cyber-Physical Systems
Differential equation invariance axiomatization (J.ACM)15-424: Logical Foundations of Cyber-Physical Systems (Fa'21)
Differential Game Logic for Hybrid GamesLogical Foundations of Cyber-Physical Systems
Case Study: Formal verification of obstacle avoidance and navigation of ground robots (IJRR'17)Case Study: 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 Software: A Hybrid Theorem Prover for Hybrid SystemsBook: Logical Analysis of Hybrid Systems

The KeYmaera X aXiomatic Theorem Prover for Hybrid Systems is a verification tool. It is based on differential dynamic logic, which provides the Logical Foundations of Cyber-Physical Systems as explained in a recent textbook.

If you want to do research with me, you should take the Logical Foundations of Cyber-Physical Systems course, read the textbook and/or watch the video lectures.

My publications are available in the List of Publications (also see Reading Guide).

Announcements

More: Read about this research in the news.