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, Formal Methods, Theorem Proving

 

Overview

On these web pages, you will find a selection of my research topics. Not all of my research is reflected, but you will find an overview of my research agenda and can explore more 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 Verification Tool for Hybrid Systems, its brand-new successor KeYmaera X are described along with the family of differential dynamic logics for hybrid systems verification that they implement as well as more general Logical Foundations of Cyber-Physical Systems.

Information on the courses I teach at Carnegie Mellon University can be found in the Teaching Section. My personal web pages CMU Web Page and symbolaris.com are mirrors.

Publications are available at the List of Publications.

Announcements

More: Read about this research in the news.

Copyright © by André Platzer        Last modified: 2017-08-17

Publications | Research | Tools | Courses | A. Platzer