| Table of Contents |
|---|
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 Karlsruhe Institute of Technology and founded 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)
- Alexander von Humboldt Professorship in AI, 2023
- 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
- Brilliant 10 Young Scientists Award by Popular Science Magazine 2009
- Best Paper Awards: TABLEAUX 2007 for Differential dynamic logic for verifying parametric hybrid systems, FM 2009 for Formal verification of curved flight collision avoidance maneuvers: A case study, Best Tool Paper Award at FM 2019 for Pegasus: A framework for sound continuous invariant generation, and Best Paper Award at HSCC 2022 for Verifying switched system stability with logic.
- Award of the Floyd und Lili Biava Stiftung, 2006
- Graduation with distinction, University of Karlsruhe (TH), 2004
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, FM'19, and HSCC'22. 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
| 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