Keyi Shen

I am a first-year Ph.D. student in Computer Science at Georgia Institute of Technology, advised by Prof. Glen Chou. Previously, I obtained my Master's degree from University of Illinois Urbana-Champaign, co-advised by Prof. Huan Zhang and Prof. Yunzhu Li. I obtained my dual Bachelor's degree from Zhejiang University and University of Illinois Urbana-Champaign, where I was fortunate to collaborate with Prof. Sayan Mitra.

My research focuses on advancing intelligent and trustworthy robotic systems by bridging robot learning and formal verification. Driven by this vision, I explore topics such as motion planning in robotic manipulation, neural network verification, and reachability analysis of hybrid systems.

kshen84@gatech.edu  /  Github  /  Google Scholar

We propose a novel benchmark tailored for testing the soundness of NN verifiers. It successfully identified that 2 of the top 3 ranked NN verifiers in VNN-COMP 2025 can be unsound in certain cases.

We propose a GPU-accelerated branch-and-bound (BaB) framework for long-horizon planning with neural dynamics (ND) models.

We present parallel and incremental verification algorithms for hybrid systems, which concurrently construct reachability trees and effectively reuse previous computations.

We propose an open-source tool for modeling, simulation, and verification of multi-agent hybrid systems in Python. It has been used by over 70 students in ECE 484 at UIUC.