André Platzer @ Carnegie Mellon University

André Platzer	Curriculum Vitae
Associate Professor	Email:	send email
Computer Science Department	Phone:	+1 (412) 268-1558
Carnegie Mellon University	Fax:	+1 (412) 268-5576
Pittsburgh, PA 15213-3891, USA	Office:	GHC 9103

Research interests:: Logic in Computer Science, Cyber-Physical Systems, Programming Languages, Formal Methods (more)

Overview

On these web pages, you will find a selection of my research topics and tools in computer science, mathematics, and logic. Not all of my research is reflected, but you will find a reasonable overview.

There are details about the KeYmaera Verification Tool for Hybrid Systems and the family of differential dynamic logics for hybrid systems verification as well as the Logical Foundations of Cyber-Physical Systems.

Information on the courses I teach at Carnegie Mellon University can be found in the Teaching Section. My CMU Web Page and symbolaris.com are usually in synch.

Publications are available at the List of Publications.

Announcements

NSF Workshop on CPS Verification&Validation: Industrial Challenges & Foundations (Fall 2014)
CPS V&V Grand Prix announced for
Foundations of Cyber-Physical Systems course (Fall 2014)

In the News

Read about this research in the news:

MIRI	RBR

AI 10 to Watch	ScienceNews for Kids

ACM Award	JFK50 Feature

Springer	POPCity

Today	The Tartan

PopSci	Post-Gazette

Machine Intelligence Research Institute 02/15/14: André Platzer on Verifying Cyber-Physical Systems
Robotics Business Review 05/03/13: The Technology that Could Save Robotic Surgery Millions: Software diagnostic research debugs robotic surgical systems
[pdf]
ACM TechNews 04/10/13: Technique Finds Software Bugs in Surgical Robots and Helps Developers Fix Flaws, Ensure Safety
[SCS News | CMU News]
Many sources have publicized our work.
- Med Curiositech 04/23/13: Scientists developed a process to find surgical robot bugs
- -->International Hospital Equipment & Solutions: Technique finds software bugs in surgical robots
- Tartan 04/14/13: Researcher helps improve algorithm for robotic surgeons
- CRA CCC Highlight of the Week 04/11/13: Technique Finds Software Bugs in Surgical Robots
- Robotics Trends 04/11/13: Software Verification Method Detects Bugs in Surgical Robots
- Science 360 04/09/13: Technique Finds Software Bugs In Surgical Robots And Helps Developers Fix Flaws, Ensure Safety
- Science Business 04/09/13: Software Testing Technique Devised for Surgical Robots
- NSF News from the Field 04/08/13: Technique Finds Software Bugs in Surgical Robots and Helps Developers Fix Flaws, Ensure Safety
- Slashdot 04/08/13: Scientists Tout New Way To Debug Surgical Bots
- Bio-Medicine 04/08/13: Technique finds software bugs in surgical robots and helps developers fix flaws, ensure safety
- Robotics Business Review 04/08/13: Researchers Diagnose Software Bugs in Surgical Robots
- NetworkWorld 04/08/13: Scientists tout advanced process to find surgical robot bugs before the bot cuts off something important
- Science Newsline 04/08/13: Technique Finds Software Bugs in Surgical Robots And Helps Developers Fix Flaws, Ensure Safety
- Science Daily 04/08/13: Technique Finds Software Bugs in Surgical Robots and Helps Developers Fix Flaws, Ensure Safety
- Futurity 04/08/13: Find and fix ‘bugs’ in surgical robots
Look out for the tutorial about Logics of Dynamical Systems at LICS
[pdf | slides]
ScienceNews for Kids 10/11: Cars of the future
Technology Review 08/11: Perfekte Assistenzsysteme
PopSci Feature: How Intelligent Cars Will Make Driving Easier and Greener
ACM TechNews 06/21/11: Carnegie Mellon Methods Keep Bugs Out Of Software For Self-Driving Cars
[SCS news | CMU news]
Many sources have publicized our work, demonstrating the public and societal demand for safety in the technologies of the future. While some of these reports have exaggerated the results of our research, we do believe that our work is an important step toward safer vehicles and safer technology.
- ExtremeTech: CMU develops self-driving cars that are impossible to crash
- IEEE Spectrum Robotics Automaton: CMU Develops Autonomous Car Software That's Provably Safe
- Übergizmo: CMU Develops Self-Driving Cars That Are Impossible To Crash
Look out for the upcoming tutorial about KeYmaera verification at CAV'11
IEEE Intelligent Systems' AI's 10 to Watch
[pdf | doi]
NSF CAREER Award
Featured in JFK 50 Legacy Gallery: Celebrate the past to awaken the future feature in Science & Innovation, John F. Kennedy Presidential Library and Museum
[SCS news]
ACM Doctoral Dissertation Honorable Mention Award for the dissertation Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems
[SCS news]
Book on Logical Analysis of Hybrid Systems has appeared with Springer
Cover Story: Check this Out, Carnegie Mellon Today, July 2010, Vol. 7(3)
Open-DO News: Formal Methods Week 2009
LfSA Workshop
Best Paper Award at FM'09
Tartan: Professor included in Pop Sci's Brilliant 10
POPCity Innovation News: Carnegie Mellon's "crash test anti-dummy" named to Brilliant 10
AMS Math Digest -- Summaries of Media Coverage of Math
Brilliant 10 in Popular Science Magazine, November 2009
CMU News: Platzer Honored for Systems Research
Pittsburgh Post-Gazette: CMU professor recognized for making things miss
CMU SCS News 10/15/2009: Popular Science Chooses Carnegie Mellon's Platzer For 2009 “Brilliant 10” List of Young Scientists
NSF Expedition Award
Tribune Review
Carnegie Mellon University press release: Carnegie Mellon Computer Scientists Develop Method for Verifying Safety of Computer-Controlled Devices
ACM TechNews 04/24/2009: Carnegie Mellon Computer Scientists Develop Method for Verifying Safety of Computer-Controlled Devices
NSF News 04/20/2009: Carnegie Mellon Scientists Develop Method for Verifying Safety of Computer-controlled Devices
Dr. Dobb's Portal
The Engineer Online
Communications of the ACM News 04/21/2009: Method For Verifying Safety Of Computer-Controlled Devices Developed
NetworkWorld
More than 25 other news sources