CPS V&V I&F Workshop 2017: Program

The CPS V&V Industrial Challenges and Foundations workshop will include a panel session as well as several talks from experts in industry and academia. These talks are meant to set the stage for discussions to be held at the workshop.

Note: this schedule is tentative and is subject to change. Check back here for future updates to the program and schedule.

Thursday, May 11 (optional)

Carnegie Mellon University
13:00 Undergraduate students in the CMU Foundations of Cyber-Physical Systems course will present their final projects to a panel of experts in CPS for the CPS V&V Grand Prix.

Friday, May 12

Carnegie Mellon University
09:00 Welcome and Workshop overview - André Platzer

Session I: Runtime and Complex Systems Verification

Sagar Chaki: Verifying Cyber-Physical Systems by Combining Software Model Checking with Hybrid Systems Reachability

Taylor Johnson: Real-Time Reachability for Safety Verification of Autonomous Cyber-Physical Systems

Stefan Mitsch: ModelPlex: Verified Runtime Monitors and Verified Test Oracles for Safety of Cyber-Physical Systems

10:45 Coffee Break Discussion

Session II: Aircraft and AI Verification and Certification

David Dill: Towards formal verification of Deep Neural Networks

Kristin Rozier: Safe CPS Implementation: How Do We Measure That?

12:30 Lunch Discussion

Session III: Communication and Memory Security

Stephen Magill: Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System

Saman Zonouz: Trustworthy Critical Infrastructures via Physics-Aware Just-Ahead-Of-Time Verification

Lennart Beringer (short talk): Verification using the VST

14:45 Coffee Break Discussion

Session IV: Simulation- and Testing-Based Methods

Jim Kapinski: Emerging cyber-physical system V&V challenges

Patricia Derler: From Requirements to Testing, Validation and Verification

Sridhar Duggirala: Scalable Dynamic Analysis for Large Linear Systems

Ivan Ruchkin (short talk): IPL: A Language for Model Integration Properties in Cyber-Physical Systems

17:15 Summary Discussion
17:45 Workshop end


The primary purpose of each talk should be to give context to and provide background for the full group discussions. In order to meet the goals of this workshop, we will feature two kinds of talks: solutions talks and challenge talks. These talks should generally adhere to the following guidelines.

Solution talks should introduce:

  1. The technical core idea behind the V&V and/or correct implementation approach.
  2. A qualitative critical assessment of its applications.
  3. Future challenges for safe implementation of CPS that can be connected with emerging techniques such that our community can focus on the most pressing bottlenecks with the biggest potential impacts.
Application challenge talks should introduce:
  1. Background on the fundamental technical characteristics of the particular application domain.
  2. An overview of current use of V&V and safe implementation techniques in the application domain.
  3. Future possibilities for V&V in the application domain, including a discussion on the blocking factors that need to be resolved.