Welcome
I am a Senior Principal Scientist at Toyota Research Institute of North America (TRINA) in Ann Arbor, Michigan. My research interests include Testing and Verification of Cyber-Physical Systems (CPS), Temporal Logics, and Motion Planning and Control for Autonomous Systems. Over the past few years, I have worked on verification and synthesis methods for autonomous mobile systems to support future mobility initiatives. In particular, applying formal methods in the perception - planning - control loop in open-world environments.
I have served on the program committee for AAAI 23, HSCC 23, HSCC 22, NFM 23, NFM 22. I have chaired repeatability evaluation for HSCC 2021, HSCC 2020.
Publications
Quantitative Verification of Learning-Enabled Systems using ProbStar Reachability
FiReFly: Fair Distributed Receding Horizon Planning for Multiple UAVs
Fair-CoPlan: Negotiated Flight Planning with Fair Deconfliction for Urban Air Mobility
Safe Model Predictive Diffusion with Shielding
LogSTOP: Temporal Scores over Prediction Sequences for Matching and Retrieval
Performance-Guided Refinement for Visual Aerial Navigation using Editable Gaussian Splatting in FalconGym 2.0
Scalable Multi-Agent Path Finding for Delivery Robot Systems with Temporal and Edge Capacity Constraints on Weighted Graphs
GPU-Accelerated Barrier-Rate Guided MPPI Control for Tractor-Trailer Systems
STL-GO: Spatio-Temporal Logic with Graph Operators for Distributed Systems with Multiple Network Topologies
Conformal Prediction in the Loop: Risk-Aware Control Barrier Functions for Stochastic Systems with Data-Driven State Estimators
ProbStar Temporal Logic for Verifying Complex Behaviors of Learning-enabled Systems
BR-MPPI: Barrier Rate guided MPPI for Enforcing Multiple Inequality Constraints with Learned Signed Distance Field
StarV: A Qualitative and Quantitative Verification Tool for Learning-Enabled Systems
Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications
Safe Navigation in Uncertain Crowded Environments Using Risk Adaptive CVaR Barrier Functions
Research Areas
Safe Learning-Based Control
Control Theory + Machine Learning
Developing methods that combine the performance of learning-based controllers (like Neural Networks) with the safety guarantees of formal control theory.
Autonomous Systems
Multi-Agent Systems
Designing algorithms for coordination, planning, and control of multiple autonomous agents in complex, dynamic environments.
Formal Methods
Verification & Synthesis
Applying rigorous mathematical techniques to specify, develop, and verify software and hardware systems.
Runtime Monitoring
System Health & Safety
Techniques for observing system behavior during execution to detect violations of safety properties or performance requirements.
Teaching
This course focused on the verification and testing of Cyber-Physical Systems (CPS). Topics included: Hybrid Automata, Reachability Analysis, Temporal Logics (LTL, MTL, STL), Falsification, and Data-Driven Verification.
View Course Page →Software
CBFKit: A Control Barrier Function Toolbox
Build advanced, safe robotic systems with CBFKit. Powered by JAX, this extensible Python/ROS2 toolbox integrates CBFs (including with MPPI!), supports diverse robots, controllers, sensors, and estimators.
S-TaLiRo: Toolbox for Testing and Verification of CPS
S-TaLiRo is a toolbox for Matlab/Simulink that supports testing and verification of hybrid and continuous Cyber-Physical Systems using Metric Temporal Logic (MTL). Widely used in automotive and medical domains.
VERITEX: Deep Neural Network Verification
Veritex is a Python toolbox for verification and automated repair of Deep Neural Networks, supporting both exact and over-approximate analysis of reachable outputs.
NDF-CoRoCo: Cooperative Perception
Companion codebase for the paper 'NDF-CoRoCo: Cooperative Perception and Recognition Using Neural Density Fields'. Focuses on cooperative perception using Neural Density Fields for robotics applications.
Contact
Get in Touch
I am always open to discussing new research collaborations, speaking opportunities, or questions about my work.