| Table of Contents |
|---|
Current Research Projects (Selection)
NSF Small: Sound Invariants
Sound Invariant Generation for Continuous and Hybrid Systems| Principal Investigators | André Platzer (CMU) |
| Support | NSF CNS-1739629 |
This project considers the pragmatic challenge of broadening the reach and general accessibility of cyber-physical system (CPS) analysis. It capitalizes on logical foundations for cyber-physical systems to study automated analysis for CPS without sacrificing correctness of the analysis results. While the complexities of CPSs can be quite demanding, there is a considerable pragmatic difference between rigorous reasoning techniques that are available to verification experts compared to techniques that provide a vast amount of automation support to become more accessible for novices and more productive for experts. This project focuses on finding invariants, which convey crucial insights about quantities or relationships, such as minimum safety distances, that do not change while the CPS drives or flies.
Past Research Projects (Selection)
NSF Breakthrough: Knowledge-CPS
Knowledge-Aware Cyber-Physical Systems| Principal Investigators | André Platzer (CMU) |
| Support | NSF CNS-1446712 |
This project addresses the foundational problem of knowledge and limits of knowledge within cyber-physical systems (CPS). A single system observes its environment through sensors and interacts through actuators. Neither is perfect. Thus, the CPS's internal view of the world is blurry and its actions are imprecise. CPS are still analyzed with methods that do not distinguish between truth in the world and an internal view thereof, resulting in a mismatch between the behavior of theoretical models and their real-world counterparts. How could they be trusted to perform safety-critical tasks? This project addresses this critical insufficiency by developing methods to reason about knowledge and learning in CPS.
FLI: Verifying AI-based CPS
Faster Verification of AI-based Cyber-physical Systems| Principal Investigators | André Platzer (CMU) |
| Support | Future of Life Institute |
The most exciting and impactful uses of artificial intelligence (AI) that will affect everybody in crucial ways involve smart decision making to help people in the real world, such as when driving cars or flying aircraft, or help from robots engaging with humans. All of these have a huge potential for making the world a better place but also impose considerable responsibility on the system designer to ensure it will not do more harm than good because its decisions are sometimes systematically unsafe. Responsibly allowing mankind to rely on such technology requires stringent assurance of its safety. A nontrivial enterprise for the decision flexibility in AI. The goal of this research project is to develop formal verification and validation technology that helps ensure safety, robustness, and reliability of AI-based system designs. The world is an uncertain place. So perfect performance cannot always be guaranteed in all respects. But good system designs do not compromise safety when their performance degrades. The PI is proposing to advance his verification tool KeYmaera that has been used successfully for systems known as cyber-physical systems (combining computer decisions with physics or motion) toward the additional challenges that a deep integration of AI into those systems provides. (more)
NSF CAREER: LFCPS
Logical Foundations of Cyber-Physical Systems (LFCPS)| Principal Investigators | André Platzer (CMU) |
| Support | NSF CNS-1054246 |
This project develops logical foundations for cyber-physical systems (CPS), i.e., systems that combine cyber aspects such as communication and computer control with physical aspects such as movement in space. CPS applications abound. Ensuring their correct functioning, however, is a serious challenge. Scientists and engineers need analytic tools to understand and predict the behavior of their systems. That's the key to designing smart and reliable control. By providing such analytic foundations, this project addresses an intellectual grand challenge that has substantial scientific, economical, societal, and educational impact arising from the benefits of improved CPS analysis and design. In order to tame their complexity, this project studies CPS as multi-dynamical systems, i.e., in terms of the elementary dynamical aspects of their parts.
DARPA HACMS: HA-Spiral
High Assurance Spiral: Scalable and Performance Portable Domain-Specific Control System Synthesis| Principal Investigators | Franz Franchetti (CMU) Soummya Kar (CMU) José Moura (CMU) André Platzer (CMU) Manuela Veloso (CMU) David Padua (UIUC) Jeremy Johnson (Drexel) |
| Support | DARPA HACMS AFRL FA8750-12-2-0291 |
This project studies the verified synthesis of high assurance implementations of controllers for vehicular systems that are executed in today's and future embedded and high performance embedded system processors. (more)
CMU Lablet: SOSL
Science of Security Lablet:Security Reasoning for Distributed Systems with Uncertainties
The broad goal of the Science of Security Lablet (SOSL) is to identify scientific principles that can lead to approaches to the development, evaluation, and evolution of secure systems at scale. The focus on scalability derives from a recognition that modern software-intensive systems have more components and a greater diversity of suppliers. The theme of scalability includes two principal areas of focus, which are composability and usability.
U.S. DOT UTC: T-SET
Technologies for Safe and Efficient Transportation (T-SET)| Principal Investigators | Jacobo Bielak (CMU, CEE) Jim Garrett (CMU, CEE) Robert Hampshire (CMU, Heinz) Martial Hebert (CMU, Robotics) Chris Hendrickson (CMU, CEE) Ramayya Krishnan (CMU, Heinz) Lavanya Marla (CMU, Heinz) Christoph Mertz (CMU, Robotics) Andre Platzer (CMU, CS) Raj Rajkumar (CMU, ECE, Robotics, CyLab) Paul Rybski (CMU, Robotics) Steve Smith (CMU, Robotics) Aaron Steinfeld (CMU, Robotics) Ozan Tonguz (CMU, ECE) Rahul Mangharam (University of Pennyslvania) Jianbo Shi (University of Pennyslvania) Kostas Danillidis (University of Pennyslvania) C.J. Taylor (University of Pennyslvania) Vijay Kumar (University of Pennyslvania) |
| Support | U.S. Department of Transportation DTRT12GUTC11 |
The long-term vision of this project is one of "vehicles that do not crash." About 35,000 lives are lost every year due to road accidents in the US. In intersections alone, there are about 8,500 fatalities. More than a million accidents and injuries per year take a major toll on productivity. Most accidents occur due to human errors such as distractions, tiredness or other forms of impairment. Traffic delays cause driving commuters to spend an aggregate week stuck in traffic every year, leading to huge losses in productivity. See T-SET Team at Carnegie Mellon University and University of Pennsylvania
NSF GOALI: ArchCPS
An Architecture Approach to Heterogeneous Verification of Cyber-Physical Systems| Principal Investigators | Bruce Krogh (CMU) David Garlan (CMU) André Platzer (CMU) |
| Support | NSF CNS-1035800 |
This project studies the role of architecture and heterogeneity in the verification of cyber-physical systems.
NSF Expedition: CMACS
Computational Modeling and Analysis for Complex Systems (CMACS)Next-Generation Model Checking and Abstract Interpretation with a Focus on Embedded Control and Systems Biology
| Principal Investigators | Edmund M. Clarke (CMU) Bruce Krogh (CMU) Elizabeth Cherry (Cornell) André Platzer (CMU) James Faeder (University of Pittsburgh) Nancy Griffith (CUNY) Steve Marcus (University of Maryland) Tontong Wu (University of Maryland) Rance Cleaveland (University of Maryland) Robert Gilmour (Cornell) Flavio Fenton (Cornell) James Glimm (Stonybrook) Scott Smolka (Stonybrook) Radu Grosu (Stonybrook) Klaus Havelund (NASA JPL) Gerard Holtzmann (NASA JPL) Bud Mishra (NYU) Patrick Cousot (NYU) Amir Pnueli (NYU) |
| Support | NSF CNS-0926181 |
The NSF Expedition CMACS on Computational Modeling and Analysis for Complex Systems addresses analysis of advanced technical and natural systems including complex embedded systems and biological systems. See CMACS Team at Carnegie Mellon University, CUNY, NYU, Stony Brook University, University of Maryland, Cornell, NASA JPL
NSF: Distributed Hybrid Systems
Compositionality and Reconfiguration for Distributed Hybrid Systems| Principal Investigators | André Platzer (CMU) Edmund M. Clarke (CMU) |
| Support | NSF CNS-0931985 |
This project studies compositionality challenges and distributed hybrid systems proving.
DARPA META II: Prismatic
Unified Hierarchical Probabilistic Verification Tool| Principal Investigators | David J. Musliner (SIFT) Edmund M. Clarke (CMU) Marta Kwiatkowska (Oxford) David Parker (Oxford) André Platzer (CMU) Eric Engstrom (SIFT) Paolo Zuliani (CMU) |
| Support | DARPA FA8650-10C-7077 |
This project develops PRISMATIC, a unified tool and technique for formal design verification, as an extension of PRISM for statistical model checking.
ONR: Statistical Model Checking
Statistical Model Checking and Synthesis of Networked Cyber-Physical Systems| Principal Investigators | Edmund M. Clarke (CMU) David J. Musliner (SIFT) André Platzer (CMU) |
| Support | ONR N00014-10-1-0188 |
This project develops statistical model checking of networked cyber-physical systems.
DFG SFB/TR: AVACS
Automatic Verification and Analysis of Complex Systems (AVACS)André Platzer has been a research assistant in the Correct System Design group of Prof. Ernst-Rüdiger Olderog at the University of Oldenburg, Germany. André's research ambitions on hybrid and real-time systems are connected with the Transregional Collaborative Research Center SFB/TR AVACS, which is led by Director Prof. Werner Damm. The project AVACS (Automatic Verification and Analysis of Complex Systems) is a collaborative research project of the Universities of Freiburg, Oldenburg, and Saarbrücken, and the Max-Planck Institute für Informatik in Saarbrücken. It addresses the rigorous mathematical analysis of models of complex safety critical computerized systems, such as aircrafts, trains, cars, or other artifacts, whose failure can endanger human life. The aim is to raise the state of the art in automatic verification and analysis techniques from its current level, where it is applicable only to isolated facets (concurrency, time, continuous control, stability, dependability, mobility, data structures, hardware constraints, modularity, levels of refinement), to a level allowing a comprehensive and holistic verification of such systems. In this project, André Platzer primarily focused on logic-based verification of hybrid systems.
DFG: KeY
The KeY Project: Integrated Deductive Software DesignThe minor thesis and diploma thesis of André Platzer have been supervised by Prof. Peter Schmitt and Prof. Bernhard Beckert in the context of the KeY project. The goal of the KeY project is to develop a comprehensive tool supporting formal specification and verification of object-oriented Java Card programs within a commercial platform for UML/JML-based software development. This approach is based on the design-by-contract paradigm. In KeY, contracts are verified statically using a semi-automatic, interactive theorem prover on the basis of a dynamic logic. André Platzer developed a sound and relatively complete calculus for object-oriented program verification. He also worked on logic-based specification-extraction, with which logical specifications can be synthesized from object-oriented programs.