I'm a third year graduate student in the ECE program at Illinois. I work in Sayan Mitra's group at the Coordinated Science Lab.

My research interests are primarily in Control and Verification of Hybrid Systems. In particular, I'm developing control algorithms and models for autonomous vehicles and applying formal methods to rigorously demonstrate the safety of these systems.

I received my BS in ECE from the University of Arizona in 2015. As a proud wildcat, born and raised in Tucson, I'll always consider Tucson my home.


At CSL, I'm working on...

Formally provable MPC schemes

Model predictive control provides an optimal solution for driving dynamical systems that also guarantees constraints on the system's behavior are obeyed. However, as the system model and/or its constraints becomes more complex, MPC becomes a computationally expensive and it becomes unclear what solution will actually be found at runtime.
I'm exploring ways to relax the optimization problem, compute closed-form solutions, and apply formal verification schemes to the problem to check that all possible behaviors of the system do obey the constraints.

Distributed Robotic Systems

The CyPhyHouse team is developing a high-level programming language framework (Koord) for streamlining development of distributed robotic applications. This makes the process accessible to a wider demographic (e.g. appropriate for education/outreach), enables researchers to efficiently test algorithms on virtually any robot platform, and lays a foundation for us to incorporate verification at compile time.
I am assembling a fleet of small-scale autonomous ground vehicles (based off the F1/10 platform) called ARCaDe, on which we will deploy and test Koord.

Safe autonomous satellite rendezvous

During my internship at the Air Force Research Lab (2016), I studied a benchmark hybrid model of a fundamental maneuver for autonomous spacecraft navigation called Rendezvous. I modeled the system and its constraints to run through well-established verification tools: C2E2 and SpaceEx. Furthermore, I implemented an alternate reachability algorithm for this spacecraft problem in Matlab (dubbed SDVTool). Overview of this work and related past work can be found here. I presented this work at the ARCH workshop of the 2017 CPS Week conference.

Driving cars with a neural network

This concept has been around since ALVINN in the 90s and continues to be a popular, promising approach. We are exploring this option for controlling the ARCaDe cars. We have modeled CSL and one of the cars in the Unity gaming engine, and are training and testing in the game world. We'd like to study the effects and nature of adversarial examples using the controlled environment in Unity.


Verified hybrid LQ control for autonomous spacecraft rendezvous. Nicole Chan and Sayan Mitra. In the 56th IEEE Conference on Decision and Control (CDC 2017).

Verifying safety of an autonomous spacecraft rendezvous mission. Nicole Chan and Sayan Mitra. In the 4th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH 2017).

CODEV: Automated Model Predictive Control Design and Formal Verification (Tool Paper). Nicole Chan and Sayan Mitra. In the 21st International Conference on Hybrid Systems: Computation and Control (HSCC 2018).

Design and Verification of a Safe Autonomous Satellite Rendezvous Maneuver (MS Thesis). Nicole Chan.


Download PDF


CODEV: Matlab tool for synthesizing and verifying model predictive control (MPC)

ROS workspace for the original F1/10 car build

and the modified second build.

Full software stack for the CyPhyHouse project (implemented on the aforementioned cars as well as quadcopters).


Get in touch

247 Coordinated Science Lab

1308 W Main Street
Urbana, IL 61801