André Platzer @ Carnegie Mellon University

About André Platzer

André Platzer has joined the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA, USA, as an assistant professor in 2008. He is working on verification of hybrid systems, and is particularly interested in logic-based methods, integration of automated theorem proving and model checking, and algebraic techniques.

Dr. Platzer has developed the theory, practice, and applications of logic-based verification of hybrid systems, and he proved the first completeness theorem for hybrid systems. He introduced compositional verification techniques and methods that can verify hybrid systems without solving their differential equations (differential invariants). In addition, he developed the first theorem prover for hybrid systems (KeYmaera). Dr. Platzer has verified aircraft and train control systems.

From 2004 till 2008, André Platzer has been at the University of Oldenburg, Germany, in the Transregional Collaborative Research Center AVACS of the Universities of Freiburg, Oldenburg, and Saarbrücken, and the Max-Planck Institute für Informatik in Saarbrücken. He was also a member of the Graduate School on Trustworthy Software Systems. Dr. Platzer did is his PhD in logic-based hybrid systems verification.

Previously, he studied at the University of Karlsruhe (TH), Germany, and the University of Oldenburg, Germany. Mr. Platzer has received a Diploma degree (equiv. to MSc.) in computer science from the University of Karlsruhe (TH), Germany, in 2004, with a minor in mathematics. During his studies, he specialized in logic and theoretical fundamentals, as well as compiler construction, software engineering, and abstract algebra. He worked on other advanced topics in areas like theorem proving, verification, computer algebra, algebraic geometry, nonlinear optimization, machine learning, and algorithm engineering.

Research Interests

verification of hybrid systems, automated theorem proving, model checking, dynamic logic, modal logic, hybrid logic, decision procedures, quantifier elimination in real-closed fields, computer algebra and symbolic computation, differential algebra, differential equations, model theory, verification of object-oriented systems, verification algorithms    (Details)

Publications

List of Publications
[DBLP | Google Scholar | CiteSeer]

Curriculum Vitae (short cv)

Some Research Projects and Activities

CMU

André Platzer is a faculty member in the School of Computer Science at Carnegie Mellon University. In joint work with Prof. Edmund M. Clarke, he is working on verification techniques for hybrid systems and applications, including challenging areas like air traffic control. Hybrid systems have interaction discrete and continuous transitions. This includes cyber-physical systems with computerized control of physical systems, for instances cars, aircraft, trains. Analyzing their correct functioning is crucially important, because malfunctions can cause fatal injuries.
See current research and associated research-oriented courses.

AVACS

As a research assistant in the Correct System Design group of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg, Germany, André's research ambitions have been placed in the Transregional Collaborative Research Center SFB/TR AVACS, which is led by Director Prof. Werner Damm. The project AVACS (Automatic Verification and Analysis of Complex Systems) addresses the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. The aim is to raise the state of the art in automatic verification and analysis techniques from its current level, where it is applicable only to isolated facets (concurrency, time, continuous control, stability, dependability, mobility, data structures, hardware constraints, modularity, levels of refinement), to a level allowing a comprehensive and holistic verification of such systems. In this project, André Platzer primarily focused on the logic-based verification of hybrid systems.

KeY

Both the minor thesis and diploma thesis of André Platzer have been supervised by Prof. Peter Schmitt and Prof. Bernhard Beckert in the context of the KeY project. The goal of this joint research project is to develop a comprehensive tool supporting formal specification and verification of object-oriented Java Card programs within a commercial platform for UML/JML-based software development. This approach is based on the design-by-contract paradigm. In KeY, contracts are verified statically using a semi-automatic, interactive theorem prover on the basis of a dynamic logic. André Platzer developed a sound and relatively complete calculus for object-oriented program verification and further worked on logic-based specification-extraction.