André Platzer @ Carnegie Mellon University

André Platzer @ Carnegie Mellon University
Table of Contents
  1. André Platzer
    1. Research Interests
    2. Curriculum Vitae
    3. Honors and Awards (Selection)
    4. Biographical Sketch
    5. Publications
    6. Press Coverage
    7. Research Projects (Selection)
    8. Invited Talks, Tutorials & Lectures
    9. Conferences
    10. Teaching
    11. Advising

André Platzer

Address:André Platzer
Computer Science Department
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213-3891
Office:GHC 9103
Phone:+1 (412) 268-1558
Fax:+1 (412) 268-5576
Email:send email

Name: Sammi DiNardo
Office: GHC 9118
Phone: +1(412) 268-7660
Email: sdinardo@cs.cmu....

My primary appointment is in the Computer Science Department at CMU, with courtesy appointments in the Robotics Institute and in Electrical & Computer Engineering.

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
Assistant Professor of Computer Science at Carnegie Mellon University CV
2008 Ph.D. degree, summa cum laude, in computer science from the University of Oldenburg
ACM Doctoral Dissertation Honorable Mention Award
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)

Biographical Sketch

André Platzer is an Assistant Professor of Computer Science at Carnegie Mellon University, Pittsburgh, PA, USA. He develops the logical foundations of cyber-physical systems to characterize their fundamental principles and to answer the question how we can trust a computer to control physical processes. His interests include logic in computer science, cyber-physical systems, programming languages, formal methods, and automated theorem proving.

Dr. Platzer developed a family of logics for dynamical systems, collectively known as differential dynamic logics for multi-dynamical systems. Differential dynamic logics were instrumental in developing a substantially richer theory of cyber-physical systems. They can be used in practice to analyze cyber-physical systems to guarantee correct interactions of a computer with the physical world. He led the development of the theorem prover KeYmaera, which has been used for verification in automotive, railway, and aviation transportation systems, as well as autonomous and surgical robotics.

André Platzer received an undergraduate and master's degree in computer science from the University of Karlsruhe (TH), Germany, in 2004, and a Ph.D. in computer science from the University of Oldenburg, Germany, in 2008, after which he joined the faculty at Carnegie Mellon University as an Assistant Professor in the Programming Languages and the Formal Methods groups of the Computer Science Department.

Dr. Platzer received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, the Best Paper Awards at TABLEAUX'07 and at FM'09. He 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.


List of Publications
[DBLP | Google Scholar | by year | by area | abstracts | guide]

Press Coverage

See page with news coverage.

Research Projects (Selection)

High Assurance Spiral: Scalable and Performance Portable Domain-Specific Control System Synthesis (DARPA HACMS)
Technologies for Safe and Efficient Transportation. (US DOT)
Science of Security Lablet:
Security Reasoning for Distributed Systems with Uncertainties
Logical Foundations of Cyber-Physical Systems (NSF CAREER)
An Architecture Approach to Heterogeneous Verification of Cyber-Physical Systems (NSF GOALI)
Distributed Hybrid Systems
Compositionality and Reconfiguration for Distributed Hybrid Systems
Computational Modeling and Analysis for Complex Systems. (NSF EXPEDITION)


Invited Talks, Tutorials & Lectures

MAP-i (Invited Spring School on "Logic of Dynamical Systems"), Universidade do Minho, Braga, Portugal, March 24-28, 2014
ENS Lyon (Invited Research School on "Logic of Dynamical Systems"), École Normale Supérieure (ENS) de Lyon, France, January 20-24, 2014
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
EPCL 2012 (Invited Lecture and Invited Course) European PhD Program in Computational Logic, Basic Training Camp, Dresden, December 10-21
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
LICS 2012 (Invited Tutorial) Dubrovnik, Croatia, June 24-28
FroCoS 2011 (Invited Tutorial) Saarbrücken, Germany, October 5-7
CAV 2011 (Invited Tutorial) Cliff Lodge, Snowbird, Utah, July 14-20
ACA 2011 (Invited Talk) Houston, Texas, June 27-30
CDC/W4 2010 (Invited Tutorial) Verification of Control Systems at CDC, Atlanta, Georgia, December 15-17
VERIFY 2010 (Invited Talk) Edinburgh, UK, July 20-21
PSPL 2010 (Invited Talk) Edinburgh, UK, July 10


NFM 2014 (PC Member) Houston, TX, April 29 - May 1
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
HSCC 2013 (PC Member) Philadelphia, USA, April 8-11
FM 2012 (PC Member) Paris, France, August 27-31
LfSA 2012 (PC Chair) Berkeley, CA, July 7, 2012
HSCC 2012 (PC Member) Bejing, China, April 17-19
FTP 2011 (PC Member) Bern, Switzerland, July 4
TABLEAUX'11 (PC Member) Bern, Switzerland, July 4-8
FMOODS & FORTE 2011 (PC Member) Reykjavik, Iceland, June 6-9
HSCC 2011 (PC Member) Chicago, USA, April 12-14
FORMATS'10 (PC Member) Vienna, Austria, September 8-10, 2010
IJCAR 2010 (PC Member) Edinburgh, Scotland, July 16-19, 2010
LfSA 2010 (PC Chair) Edinburgh, Scotland, July 15, 2010
HSCC 2010 (PC Member) Stockholm, Sweden, April 12-16, 2010


Principles of Imperative Computation Spring'14
Foundations of Cyber-Physical Systems, ENS Lyon, Spring'14
Foundations of Cyber-Physical Systems Fall'13
Principles of Imperative Computation Spring'13
Compiler Design Fall'12
Principles of Imperative Computation Spring'12
Compiler Design Fall'11
Logical Analysis of Hybrid Systems Spring'11
Compiler Design Fall'10
Modal Logic Spring'10 (jointly with Frank Pfenning)
Data, Code, Decisions Fall'09
Hybrid Systems Analysis and Theorem Proving Spring'09
See list of courses.


See web page of our group: Logical Systems Lab.