15-424: Logical Foundations of Cyber-Physical Systems (Fa'18)

Table of Contents
  1. Final Project Schedule
  2. Project Teasers
  3. Awards

Final Project Schedule

The Fall 2018 students of the CMU 15-424/624/824 Foundations of Cyber-Physical Systems course are competing in the CPS V&V Grand Prix with the following self-defined final course projects on CPS verification.
GHC 6115, Carnegie Mellon University

1:00-1:20  Introduction of Judges and dL André Platzer

1:20-2:20  First Session: Verified Internet-of-Things

1:20Formal Verification of V2I-aided Autonomous Driving: A Hybrid Systems Approach
[paper | slides | study] Dhruv Mahajan and Ishan Pardesi
1:35Modelling Safe Left Ventricular Assist Devices
[paper | slides | study] Naina Checka and Rishabh Brajabasi
1:50Modeling the Dynamics of a Smart Dental Drill
[paper | slides | study] Sheela Hanagal and Minji Kim
2:05 Physically Motivated Safety Guarantees for Machine Knitting
[paper | slides | study] Jenny Lin

2:20-3:05   Second Session: Theory

2:20Focusing for dL
[paper | slides] Klaas Pruiksma
2:35Towards Efficient Quantifier Elimination in Mathematica
[paper | slides | study] Katherine Cordwell
2:50On Decidable Fragments of dL
[paper | slides | study] Siva Somayyajula and David Kahn

3:05-3:25   Break

3:25-3:55   Third Session: KeYmaera X Improvements

3:25KeYmaera X++: Improving the Proof Experience
[paper | slides | study] Corwin de Boor
3:40Differential-Algebraic Dynamic Logic for KeYmaera X
[paper | slides | study] Benjamin Lim and Yao Chong Lim

3:55-4:40   Fourth Session: Verified Complex Controllers

3:55Slalom: Modelling obstacle avoidance during skiing
[paper | slides | study] Naveen Pai
4:10Dynamic Equilibrium System: Atwood Machine with Spring
[paper | slides | study] Katherine Kireeva
4:25Locked-on: verifying controls for aircraft tracking
[paper | slides | study] Chun Kai Ling and Daniel L.K. Wong

4:40-5:25   Fifth Session: Verification of Large Scale Systems

4:40BusyBees: Safe Controllers for Multi-Agent Swarms
[paper | slides | study] Joshua Durham
4:55Formal Verification of Traffic Networks at Equilibrium
[paper | slides] Matthew Battifarano
5:10Statistical Model Checking for Algorithmic Trading Strategies via Simulation of Geometric Brownian Motion
[paper | slides | study] Abhishek Bhargava and Michael You

5:25-5:40   Break

5:40-6:10   Judges in Closed Session

6:10-6:40   Presentation of Awards

Project Teasers

These images are shared by the respective students in the course to illustrate the topic of their final projects.

Awards

In an amazingly tough competition with numerous verification rockstar quality projects, the judges finally settled on the following awards:
  1. Abhishek Bhargava and Michael You
  2. Corwin de Boor
  3. Katherine Cordwell
Honorable Mentions: