André Platzer

  1. Home
  2. >>
  3. A. Platzer
André Platzer
Table of Contents
  1. André Platzer
    1. Brief Biography
    2. Research Interests
    3. Academic Appointments
    4. Visiting Positions
    5. Education
    6. Honors and Awards (Selection)
    7. Biographical Sketch
    8. Publications
    9. Invited Talks, Tutorials & Lectures (Selection)
    10. Teaching
    11. Advising
    12. Journals
    13. Press Coverage (Selection)

André Platzer

Address:André Platzer
KIT Informatics Department / KASTEL
Am Fasanengarten 5
Geb. 50.34
76131 Karlsruhe
Germany
Office:Building 50.34, Room 155
Phone:20854-806 127 94+
Email:ude.tik@reztalp

Assistant:
Name: Laurence Böhnke
Office: Building 50.34, Room 160
Phone: +49 721 608-45800
Email: laurence.boehnke@kit.edu

Primary appointment KIT Department of Informatics at Karlsruhe Institute of Technology, and founder of the Logical Systems Lab at Computer Science Department at Carnegie Mellon University.

Brief Biography

André Platzer is an Alexander von Humboldt Professor at Karlsruhe Institute of Technology and founded and led the Logical Systems Lab as an Assistant/Associate/Full Professor at Carnegie Mellon University. He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes. The solution to this challenge is the key to enabling computer assistance that we can bet our lives on. Prof. Platzer pursues this challenge with the principled design of programming languages with logics that can provide proofs as correctness guarantees.

Short CV Long

André Platzer has a Ph.D. from the University of Oldenburg, Germany, received an ACM Doctoral Dissertation Honorable Mention and NSF CAREER Award, 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, and received the Alexander von Humboldt Professorship for AI 2023.

Research Interests

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

Academic Appointments

since
07/2022
Alexander von Humboldt Professor Karlsruhe Institute of Technology
07/2020-
06/2022
Full Professor of Computer Science Carnegie Mellon University
07/2014-
06/2020
Associate Professor of Computer Science Carnegie Mellon University
10/2008-
06/2014
Assistant Professor of Computer Science Carnegie Mellon University

Visiting Positions

01/2019-
08/2019
Visiting Professor of Computer Science Technical University Munich
05/2015-
08/2015
Visiting Associate Professor of Computer Science Cornell University

Education

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 Karlsruhe Institute of Technology / University of Karlsruhe (TH)
10/2001-09/2004 Master studies of computer science and mathematics at the Karlsruhe Institute of Technology / University of Karlsruhe (TH)
10/1999-09/2001 Undergraduate studies of computer science and mathematics at the Karlsruhe Institute of Technology / University of Karlsruhe (TH)

Honors and Awards (Selection)

Biographical Sketch

André Platzer is the Alexander von Humboldt Professor for Logic of Autonomous Dynamical Systems at Karlsruhe Institute of Technology leading the Institute for Reliability of Autonomous Dynamical Systems. He develops logics for dynamical systems to characterize the logical foundations of cyber-physical systems and to answer the question how we can trust a computer to control physical processes.

Short CV Long

Dr. Platzer develops 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 as an Assistant, then Associate, then Full Professor at Carnegie Mellon University in the Programming Languages and Formal Methods groups of the Computer Science Department. In 2022, André Platzer joined KIT as Alexander von Humboldt Professor.

Dr. Platzer received an ACM Doctoral Dissertation Honorable Mention Award, an NSF CAREER Award, and Best Paper Awards at TABLEAUX'07, FM'09, and FM'19. 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, and received the Alexander von Humboldt Professorship for AI 2023.

The Alexander von Humboldt Professorship, Germany's most highly endowed international research award, is endowed with up to five million euros. With this award, the Alexander von Humboldt Foundation honors internationally leading researchers of all disciplines.

Publications

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

Invited Talks, Tutorials & Lectures (Selection)

FMTea 2024 (Keynote) Formal Methods Teaching Workshop, Milano, Italy 2024 [TFM'24]
SAT/SMT/AR 2024 (Invited Lecture) SAT/SMT/AR Summer School 2024 on Satisfiability (SAT), Satisfiability Modulo Theories (SMT), and Automated Reasoning (AR), Nancy, France 2024
ABZ 2023 (Keynote), 9th International Conference on Rigorous State Based Methods (ABZ), May 30 to June 2 2023, Loria, Nancy, France [ABZ'23 | SCP'24]
VTSA 2022 (Invited Lectures 1-2, Lecture 3, Lecture 4) Summer School on Verification Technology, Systems & Applications, Max Planck Institute for Informatics, Saarbrücken, September 2022
CCC 2021 (Invited tutorial) Continuity, Computability, Constructivity From Logic to Algorithms, CCC, University of Birmingham, September 2021
LFCS 2020 (Invited talk) Symposium on Logical Foundations of Computer Science, Deerfield Beach, FL, USA, January 4-7, 2020
QEST 2019 (Keynote) International Conference on Quantitative Evaluation of SysTems, Glasgow, UK, September 10-12, 2019 [QEST'19']
marktoberdorf 2019 (Invited Lectures 1‑3 and Lecture 4 and Exercises) Marktoberdorf Summer School on Safety and Security of Software Systems: Logics, Proofs, Applications, Marktoberdorf, Germany, July 31 to August 9, 2019 [MOD'19]
POPL 2019 (Contributed Tutorial) Symposium on Principles of Programming Languages POPL, Lisbon, Portugal, January 13-19, 2019
ITC 2018 (Invited Talk) International Test Conference ITC, Phoenix, October 28 - November 2, 2018 [ITC'18]
SoMLMFM 2018 (Invited Talk) FLoC Summit on Machine Learning Meets Formal Methods, Oxford University, UK, July 13, 2018
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 Lecture 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 by Nathan Fulton
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 [IJCAR'16]
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
MSR-A 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 [ITP'12]
DCFS 2012 (Keynote) Descriptional Complexity of Formal Systems, Braga, Portugal, July 23-25 [DCFS'12 | JALC'12]
LICS 2012 (Invited Tutorial) Logic in Computer Science LICS 2012, Dubrovnik, Croatia, June 24-28 [LICS'12]
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 [CAV'11]
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

See list of courses at Karlsruhe Institute of Technology or Carnegie Mellon University.

Advising

See web page of our group: Logic of Autonomous Dynamical Systems Group

Journals

Press Coverage (Selection)

See page with news coverage.