André Platzer @ Carnegie Mellon University

André Platzer

Research Interests

logic, verification of hybrid systems, verification of distributed 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 and Publications)

Conferences

Biographical Sketch

André Platzer is an Assistant Professor in the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA, USA. His interests include hybrid systems, distributed hybrid systems, logic, automated theorem proving, model checking, symbolic and numerical computation.

André Platzer developed the theory, practice, and applications of logic-based verification of hybrid systems, and he proved the very 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 led the development of the first theorem prover for hybrid systems (KeYmaera) and he has worked on verification of aircraft and train control systems.

In recent work, André Platzer has introduced the first formal verification approach for distributed hybrid systems, in which participants can appear and disappear dynamically while the system follows its hybrid dynamics.

André Platzer obtained a Master's degree in computer science (minoring in mathematics) from the University of Karlsruhe (TH), Germany, in 2004, and a Ph.D. in computer science from the University of Oldenburg, Germany, in 2008. He was involved in the research project DFG 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. His Ph.D. thesis was on logical analysis and verification of hybrid systems.

André Platzer reviews submissions for important conferences and journals in the field on a regular basis and serves on various program committees. Among other awards, he received an ACM Doctoral Dissertation Honorable Mention Award, the Best Paper Awards at TABLEAUX'07 and FM'09, the Woody Bledsoe Award, and a fellowship by the German Academic Exchange Service (DAAD). André Platzer was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009.

Publications

Curriculum Vitae (short cv)

Honors and Awards (Selection)

• ACM Doctoral Dissertation Honorable Mention Award for the dissertation Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems
• Best Paper Award at FM'09, Eindhoven, Netherlands, 2009, for Formal verification of curved flight collision avoidance maneuvers: A case study
• Brilliant 10 Young Scientists Award of 2009
• Graduation with distinction, University of Oldenburg 2008
• Best Paper Award at TABLEAUX'07, Aix-en-Provence, France, 2007, for Differential dynamic logic for verifying parametric hybrid systems
• Woody Bledsoe Award, IJCAR 2006
• FLoC 2006 Student Travel Grant, Seattle, USA
• German Academic Exchange Service (DAAD) fellowship 2006
• Award of the Floyd und Lili Biava Stiftung 2006
• Graduation with distinction, University of Karlsruhe (TH) 2004

News Coverage

Courses

15-411

Compiler Design Fall'10

15-816

Modal Logic Spring'10 (jointly with Frank Pfenning)

15-819M

Data, Code, Decisions Fall'09

15-819/18-879L

Hybrid Systems Analysis and Theorem Proving Spring'09

Large Research Projects and Activities (Excerpt)

CMACS

André Platzer is a Co-PI in the NSF Expedition CMACS on Computational Modeling and Analysis for Complex Systems. This Expedition addresses analysis of advanced technical and natural systems including complex embedded systems and biological systems. The Expedition is a collaborative research project involving Carnegie Mellon University, CUNY, NYU, Stony Brook University, University of Maryland, Cornell, NASA JPL.

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 at Logical Systems Lab.

AVACS

André Platzer has been 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 on hybrid and real-time systems were motivated by and connected with 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.