| 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 |
Administrative Associate:
| Name: | Dennis Marous |
|---|---|
| Office: | GHC 9118 |
| Phone: | +1(412) 268-7660 |
| Email: | dcm@cs.cmu.... |
Research Interests
Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Formal Methods
logical foundations of cyber-physical systems, logic of hybrid systems, logic of distributed hybrid systems, logic of stochastic hybrid systems, logic of hybrid games, theorem proving, automated deduction, 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, stochastic differential equations, differential-algebraic equations, model theory, verification of object-oriented programs, verification algorithms
(Details and Publications)
Curriculum Vitae
| since 10/2008 |
|
||
| 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 in the SFB/Transregio AVACS | ||
| 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 PhD 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
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, cyber-physical systems, programming languages, and formal methods.
André Platzer developed logics of dynamical systems, called differential dynamic logics for hybrid systems, distributed hybrid systems, stochastic hybrid systems, and hybrid games, and he studied their theory, practice, and applications. He studied the proof theory of hybrid systems and developed complete axiomatizations of relative to discrete or continuous dynamics. André Platzer introduced compositional proof techniques, including differential invariants that can verify hybrid systems without solving their differential equations. He led the development of the theorem provers KeYmaera for hybrid systems and KeYmaeraD for distributed hybrid systems that have been used successfully to verify safety-critical applications in automotive, aviation, railway, and medical and ground roboticss.
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. degree in computer science from the University of Oldenburg, Germany, in 2008. Since 2008, he has been on the faculty in the Computer Science Department at Carnegie Mellon University in the Programming Languages and the Formal Methods groups. He published a book on "Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics".
Among other awards, André Platzer 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 | by area | abstracts]
Press Coverage
See page with news coverage.Research Projects (Selection)
- HA-Spiral
- High Assurance Spiral: Scalable and Performance Portable Domain-Specific Control System Synthesis (DARPA HACMS)
- T-SET
- Technologies for Safe and Efficient Transportation. (US DOT)
- SOSL
- Science of Security Lablet:
Security Reasoning for Distributed Systems with Uncertainties - LFCPS
- Logical Foundations of Cyber-Physical Systems (NSF CAREER)
- ArchCPS
- An Architecture Approach to Heterogeneous Verification of Cyber-Physical Systems (NSF GOALI)
- Distributed Hybrid Systems
- Compositionality and Reconfiguration for Distributed Hybrid Systems
- CMACS
- Computational Modeling and Analysis for Complex Systems. (NSF EXPEDITION)
[More]
Conferences
| FM 2014 | (PC Member) Singapore, May 12-16 |
| SMC 2013 | (PC Member) Rennes, France, September 23 |
| ICALP 2013 | (PC Member, Track B) Riga, July 8-12 |
| SCSS 2013 | (PC Member) Hagenberg, Austria |
| FMRA | (Invited Talk), Workshop on Formal Methods for Robotics and Automation at RSS 2013, Berlin, June 27 |
| VSTTE 2013 | (Invited Talk) Atherton, CA, May 16-19 |
| HSCC 2013 | (PC Member) Philadelphia, USA, April 8-11 |
| EPCL 2012 | (Invited Lecture and Invited Course) European PhD Program in Computational Logic, Basic Training Camp, Dresden, December 10-21 |
| FM 2012 | (PC Member) Paris, France, August 27-31 |
| VSWSS 2012 | (Invited Course) Microsoft Research Asia, Verified Software Summer School, August 23-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'11 | (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'10 | (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 |
Teaching
- 15-424
- Foundations of Cyber-Physical Systems Fall'13
- 15-122
- Principles of Imperative Computation Spring'13
- 15-411
- Compiler Design Fall'12
- 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