| Table of Contents |
|---|
André Platzer
| Address: | André Platzer Computer Science Department Carnegie Mellon University 5000 Forbes Avenue Pittsburgh, PA 15213-3891 USA |
|---|---|
| Office: | GHC 9103 |
| Phone: | +1 (412)-268-1558 |
| Fax: | +1 (412)-268-5576 |
| Email: | send email |
Research Interests
logic, logical foundations of cyber-physical systems, 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
| FM 2012 | (PC Member) Paris, France, August 27-31 |
| ITP 2012 | (Invited Talk) Princeton, NJ, August 13-16 |
| DCFS 2012 | (Keynote) Braga, Portugal, July 23-25 |
| LfSA 2012 | (PC Chair) Berkeley, CA, July 7, 2012 |
| LICS 2012 | (Invited Tutorial) Dubrovnik, Croatia, June 24-28 |
| HSCC 2012 | (PC Member) Bejing, China, April 17-19 |
| FroCoS 2011 | (Invited Tutorial) Saarbrücken, Germany, October 5-7 |
| CAV 2011 | (Invited Tutorial) Cliff Lodge, Snowbird, Utah, July 14-20 |
| FTP 2011 | (PC Member) Bern, Switzerland, July 4 |
| TABLEAUX 2011 | (PC Member) Bern, Switzerland, July 4-8 |
| ACA 2011 | (Invited Talk) Houston, Texas, June 27-30 |
| FMOODS & FORTE 2011 | (PC Member) Reykjavik, Iceland, June 6-9 |
| HSCC 2011 | (PC Member) Chicago, USA, April 12-14 |
| CDC/W4 2010 | (Invited Tutorial) Verification of Control Systems at CDC, Atlanta, Georgia, December 15-17 |
| FORMATS 2010 | (PC Member) Vienna, Austria, September 8-10, 2010 |
| VERIFY 2010 | (Invited Talk) Edinburgh, UK, July 20-21 |
| IJCAR 2010 | (PC Member) Edinburgh, Scotland, July 16-19, 2010 |
| LfSA 2010 | (PC Chair) Edinburgh, Scotland, July 15, 2010 |
| PSPL 2010 | (Invited Talk) Edinburgh, UK, July 10 |
| HSCC 2010 | (PC Member) Stockholm, Sweden, April 12-16, 2010 |
Biographical Sketch
André Platzer is an Assistant Professor in the Computer Science Department at Carnegie Mellon University, Pittsburgh, PA, USA. His interests include logic in computer science, hybrid systems, distributed hybrid systems, automated theorem proving, model checking, symbolic and numerical computation.
André Platzer developed the theory, practice, and applications of logical analysis and 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 (called 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, railway, and car 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 with a minor 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 DFG Transregional Collaborative Research Center AVACS. He was also a member of the Graduate School on Trustworthy Software Systems. André Platzer published a book on "Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics", which is based on his Ph.D. thesis "Differential Dynamic Logics: Automated Theorem Proving for 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, an NSF CAREER Award, the Best Paper Awards at TABLEAUX'07 and at FM'09. André Platzer was also named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and was named one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.
Publications
List of Publications[DBLP | Google Scholar | Microsoft Academic Search | ACM | CiteSeer]
Curriculum Vitae (short cv)
| since 10/2008 | Assistant Professor in Computer Science Department at Carnegie Mellon University |
| 2008 | Ph.D. degree, summa cum laude, in computer science from the University of Oldenburg
ACM Doctoral Dissertation Honorable Mention Award |
| 12/2005-09/2008 | Ph.D. student in the Graduate School on Trustworthy Software Systems |
| 10/2004-09/2008 | Research assistant of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg |
| 9/2004 | Graduated with distinction, Diploma degree (equiv. to MSc.) in computer science from the University of Karlsruhe (TH) |
| 10/2001-09/2004 | Master studies of computer science and mathematics at the University of Karlsruhe (TH) |
| 10/1999-09/2001 | Undergraduate studies of computer science and mathematics at the University of Karlsruhe (TH) |
Honors and Awards (Selection)
- NSF CAREER Award, 2011
- IEEE Intelligent Systems' AI's 10 to Watch, 2010 [pdf | doi]
- Featured in JFK 50 Legacy Gallery, John F. Kennedy Presidential Library and Museum, 2011
- ACM Doctoral Dissertation Honorable Mention Award 2009 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 by the Popular Science Magazine 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
- Award of the Floyd und Lili Biava Stiftung, 2006
- Graduation with distinction, University of Karlsruhe (TH), 2004
News Coverage
See news coverage.Teaching
- 15-122
- Principles of Imperative Computation Spring'12
- 15-411
- Compiler Design Fall'11
- 15-819/18-879
- Logical Analysis of Hybrid Systems Spring'11
- 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
Advising
See the student members of the Logical Systems Lab.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 Computer Science Department at Carnegie Mellon University.
Among other things, 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 are 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) is a collaborative research project of the Universities of Freiburg, Oldenburg, and Saarbrücken, and the Max-Planck Institute für Informatik in Saarbrücken. It 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.