Research Projects of André Platzer

Table of Contents
  1. Current Research Projects (Selection)
    1. DARPA HACMS: HA-Spiral
    2. U.S. DOT UTC: T-SET
    3. CMU Lablet: SOSL
    4. NSF CAREER: LFCPS
    5. NSF GOALI: ArchCPS
    6. NSF: Distributed Hybrid Systems
    7. NSF Expedition: CMACS
  2. Past Research Projects (Selection)
    1. DARPA META II: Prismatic
    2. ONR: Statistical Model Checking
    3. DFG SFB/TR: AVACS
    4. DFG: KeY

Current Research Projects (Selection)

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.

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

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.

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.

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: 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.

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

Past Research Projects (Selection)

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 Design

The 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.