André Platzer

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

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

Assistant:
Name: Jessica Packer
Office: GHC 9006
Phone: +1 (412) 268-7660
Email: jpacker@cs.cmu.edu

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

Brief Biography

André Platzer is an Associate Professor of Computer Science at Carnegie Mellon University. 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.

André Platzer has a Ph.D. from the University of Oldenburg, Germany, received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER Award, and was named one of the Brilliant 10 Young Scientists by the Popular Science magazine and one of the AI's 10 to Watch by the IEEE Intelligent Systems Magazine.

Research Interests

Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Theorem Proving, Formal Methods
[Overview of my research agenda | Details | Publications]

Curriculum Vitae

since 07/2014
Associate Professor of Computer Science at Carnegie Mellon University CV
10/2008-06/2014 Assistant Professor of Computer Science 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
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 Associate 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 show how we can design computers that are guaranteed to interact correctly with the physical world.

Dr. Platzer developsa differential dynamic logics for multi-dynamical systems, which are instrumental in developing a substantially richer theory of cyber-physical systems. These logics 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 KeYmaera and KeYmaera X theorem provers, which have been used for verification in automotive, railway, and aviation transportation systems, as well as autonomous and surgical robotics.

André Platzer received a 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 in the Programming Languages and Formal Methods groups of the Computer Science Department.

Dr. Platzer received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, and Best Paper Awards at TABLEAUX'07 and FM'09. He was named one of the Brilliant 10 Young Scientists by the Popular Science magazine 2009 and one of the AI's 10 to Watch 2010 by the IEEE Intelligent Systems Magazine.

Publications

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

Press Coverage

See page with news coverage.

Invited Talks, Tutorials & Lectures

iFM 2017 (Invited Talk) International Conference on integrated Formal Methods iFM 2017, University of Torino, Italy, September 18-22, 2017
Marktoberdorf 2017 (Invited Lectures 1‑3 and 4 and Exercises) Marktoberdorf Summer School on Logical Methods for Safety and Security of Software Systems, Marktoberdorf, Germany, August 2-11, 2017
Additional tutorial demo with examples
CPS School 2017 (Invited Lectures) Summer School on Cyber-Physical Systems, CPS 2017, Halmstad University, Sweden, July 17-21, 2017 Video 1, video 2 and video 3
MEMOCODE 2016 (Keynote Talk) 14th ACM-IEEE International Conference on Formal Methods and Models for System Design, Indian Institute of Technology, Kanpur, November 18-20, 2016
IJCAR 2016 (Invited Talk) International Joint Conference on Automated Reasoning IJCAR 2016, University of Coimbra, Portugal, June 27-July 2, 2016
AVACS School 2015 (Invited Lecture) 2nd AVACS Autumn School, Oldenburg, Germany, September 30-October 2, 2015
AVACS 2015 (Invited Talk) AVACS Concluding Colloquium, Oldenburg, Germany, September 29, 2015
FMCAD 2015 (Invited Tutorial) Formal Methods in Computer-Aided Design FMCAD 2015, Austin, TX, USA, September 27-30
QuantLA 2014 (Invited Talk) Workshop Quantitative Logics and Automata, Dresden, Germany, October 6-10, 2014
HCSS 2014 (Invited Talk) High Confidence Software and Systems Conference 2014, Annapolis, MD, May 6-9, 2014
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 2013 (Invited Talk) Workshop on Formal Methods for Robotics and Automation at RSS 2013, Berlin, June 27
VSTTE 2013 (Invited Talk) Verified Software: Theories, Tools and Experiments VSTTE, 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) Interactive Theorem Proving ITP 2012, Princeton, NJ, August 13-16
DCFS 2012 (Keynote) Descriptional Complexity of Formal Systems, Braga, Portugal, July 23-25
LICS 2012 (Invited Tutorial) Logic in Computer Science LICS 2012, Dubrovnik, Croatia, June 24-28
FroCoS 2011 (Invited Tutorial) Frontiers of Combining Systems FroCoS 2011, Saarbrücken, Germany, October 5-7
CAV 2011 (Invited Tutorial) Computer Aided Verification 2011, Cliff Lodge, Snowbird, Utah, July 14-20
ACA 2011 (Invited Talk) Applications of Computer Algebra ACA, Houston, Texas, June 27-30
CDC/W4 2010 (Invited Tutorial) Conference on Decision and Control, Verification of Control Systems at CDC, Atlanta, Georgia, December 15-17
VERIFY 2010 (Invited Talk) 6th International Verification Workshop at IJCAR, Edinburgh, UK, July 20-21
PSPL 2010 (Invited Talk) Proof Systems for Program Logics at LICS, Edinburgh, UK, July 10

Teaching

15-414/15-614
Bug Catching: Automated Program Verification Fall'17
15-424/15-624/15-824
Foundations of Cyber-Physical Systems Spring'17
15-317/15-657
Constructive Logic Fall'16
15-424/15-624/15-824
Foundations of Cyber-Physical Systems Spring'16
15-317/15-657
Constructive Logic Fall'15
15-812
Programming Language Semantics Spring'15
15-424/15-624
Foundations of Cyber-Physical Systems Fall'14
15-122
Principles of Imperative Computation Spring'14
15-424/624
Foundations of Cyber-Physical Systems, MAP-i, Universidade do Minho, Spring'14
(one-week intensive course)
15-424/624
Foundations of Cyber-Physical Systems, ENS Lyon, Spring'14
(one-week intensive course as a research school)
15-424/15-624
Foundations of Cyber-Physical Systems Fall'13
15-122
Principles of Imperative Computation Spring'13
15-411/15-611
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
See list of courses.

Advising

See web page of our group: Logical Systems Lab.