André Platzer @ Carnegie Mellon University

André Platzer @ Carnegie Mellon University

Overview

This is the home page of André Platzer at Carnegie Mellon University.

On this web page, you will find a selection of my research topics and tools in computer science, mathematics, and logic. Especially, verification technology for hybrid systems.

KeYmaera: A Hybrid Theorem Prover for Hybrid SystemsLogical Analysis of Hybrid Systems
Logic for Distributed Hybrid Systems15-411: Compiler Design
Logic for Stochastic Hybrid SystemsCase Study: Formal Verification of Curved Flight Collision Avoidance Maneuvers

Among several other research topics, you will find details about the KeYmaera Verification Tool for Hybrid Systems and the theory of differential dynamic logic for hybrid systems verification.

This page further hosts the Orbital library for Java, which provides several object-oriented representations and algorithms for logic, mathematics and artificial intelligence. There are Java applets of strategic board games, as well as survey description documents on some aspects of computer science.

Information on the courses I teach at Carnegie Mellon University can be found in the Teaching Section.

See List of Publications for more information on publications that are related to logic, computer science, and mathematics

Announcements

In the News

Read about this research in the news:
AI 10 to Watch 2010
AI 10 to Watch
ScienceNews for Kids
ScienceNews for Kids
ACM Doctoral Dissertation Honorable Mention Award
ACM Award
JFK 50 Science & Innovation
JFK50 Feature
Logical Analysis of Hybrid Systems
Springer
POPCity Innovation
POPCity
Carnegie Mellon Today Cover Story: Check this Out
Today
The Tartan
The Tartan
Brilliant 10 in Popular Science Magazine
PopSci
Post-Gazette
Post-Gazette