CPS V&V I&F Workshop 2018: 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.

Tuesday, Dec 11 (optional)

Carnegie Mellon University
13:00 Undergraduate students in the CMU Logical 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.

Wednesday, Dec 12

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

Session I: Formal Verification of Learning CPS

Jean-Baptiste Jeannin: Verifying Aircraft Collision Avoidance Neural Networks

Taylor T. Johnson: Safety Assurance in Cyber-Physical Systems built with Learning-Enabled Components

Nathan Fulton: Verifiably Safe Reinforcement Learning

10:45 Coffee Break Discussion
11:15

Session II: Formal Methods in System Safety Processes

Aaron Kane: Towards Formalizing the System Safety Argument

Christof Budnik: Fertilized Testing of Train Braking Systems using Formal Models as Test Oracles

12:15 Lunch Discussion
13:30

Session III: Formal Methods Challenges

Kristin Rozier: Formal Methods for Common Sense: A Challenge

Grant Passmore: Formal Verification of Financial Algorithms

Jim Kapinski

15:00 Coffee Break Discussion
15:30

Session IV: Robust Control and Runtime Monitoring for Learning CPS

Brandon Bohrer: Verified Runtime Monitoring: From Foundations to Practice

Taisa Sima Kushner: Robust Data-Driven Control for Artificial Pancreas Systems Using Neural Networks

Sriharsha Etigowni: I Look at Physics and Predict Control Flow! Just-Ahead-Of-Time Controller Recovery

Chris McKinnon: Model Learning for Long-term Safe Control in Changing Environments

17:30 Summary Discussion
18:00 Workshop end

Talks

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.