CPS V&V I&F Workshop 2014: 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 end of the workshop.

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

Wednesday, December 10 (optional)

Gates-Hillman Center (GHC), Room 6115, 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.

Thursday, December 11

Gates-Hillman Center (GHC), Room 6115, Carnegie Mellon University
08:30 Light breakfast served
09:00 Welcome and Workshop overview - André Platzer
09:10 Aerospace Challenge Talks
Kristin Y. Rozier: Integration of Formal Methods into Design and Implementation of Aerospace
Jean-Baptiste Jeannin: Challenges in the Verification of Existing Aerospace Systems
Alwyn Goodloe: Challenges in the Verification of Flight-Critical Systems
10:10 Aerospace Discussion - led by Kristin Y. Rozier
11:15 Break
11:30 Automotive Challenge Talks
Jim Kapinski: Ongoing Challenges in Applying V&V Technologies to Automotive Engine Control
Thomas Heinz: Hybrid Systems Verification Challenges at Bosch
12:10 Automotive Discussion - led by Jim Kapinski
13:00 Lunch
14:00 Analysis Talks
André Platzer: Logical Foundations of Cyber-Physical Systems
Ian Mitchell: Scalable Parametric Approximations of the Maximal Controlled Invariant Set and Two Health Related Application Domains
14:40 Break
15:00 Khalil Ghorbal: Reasoning About Dynamical Systems Using Invariants: Achievements and Challenges
Sriram Sankaranarayanan: Deductive Approaches for Stochastic Systems
15:40 Foundations Discussion - led by André Platzer
18:00 Dinner

Friday, December 12

08:30 Light breakfast served
09:00 Modeling Foundations Talks
David Garlan: Multi-domain Modeling of Cyber-Physical Systems using Architectural Views
Dionisio de Niz: Analysis Contracts for CPS
09:40 Synthesis Talks
Sicun Gao: Nonlinear Control as Program Synthesis
10:00 Verification in Industry: Barriers and Successes Discussion - led by Sagar Chaki
11:00 Break
11:20 Bridging Talks
Taylor Johnson: Cyber-Physical Specification Mismatch Identification with Dynamic Analysis Systems
Stefan Mitsch: Verified runtime validation of verified cyber-physical system models
Parasara Sridhar Duggirala: Simulations to Proofs in C2E2
12:20 Discussion: Identifying Future CPS Challenges and Connecting them with Emerging Techniques - led by Bruce Krogh
14:00 Lunch
15:00 Additional Discussions and Closing Discussion
16:45 Wrap-up
17:00 Adjourn


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 approach.
  2. A qualitative critical assessment of its applications.
  3. Future CPS challenges 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 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.