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 EMSOFT 26, VehicleSec 26, RV 26, NFM 26, ICCPS/HSCC 26, RV 25, HSCC 25, HSCC 24, AAAI 23, HSCC 23, NFM 23, AutoSec 22, HSCC 22, NFM 22, MT-CPS 21, SafeThings 20, MT-CPS 20. I have chaired repeatability evaluation for HSCC 2021, HSCC 2020.
Publications
Reinforcement Learning for Risk Adaptation via Differentiable CVaR Barrier Functions
Policy Library CBF: Finite-Horizon Safety at Runtime via Parallel Rollouts
Vision-Based Runtime Monitoring under Varying Specifications using Semantic Latent Representations
Bayesian Risk-Aware CBFs for Discrete-Time Stochastic Systems with Learned Dynamics
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
Spatio-Temporal Grounding of Large Language Models from Perception Streams
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
Patents
Systems and methods for risk-bounded control barrier functions
Methods and systems for spatio-temporal regular expression matching
Systems and methods for online monitoring using a neural model by an automated vehicle
Producing a simulation recording to test an automated driving system
System and method for safe control synthesis for hybrid systems through local control barrier functions
Systems and methods for predictive risk-aware control of vehicles in dynamic environments
Learning abstractions for multi-robot path planning in unstructured environments
Systems and methods for control barrier functions for enhanced feasibility in optimization-based control
Timed partial order identification for task learning from data
Neural network verification for neural network controllers
Temporal logic robustness guided testing for cyber-physical systems
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.
TLTk: Parallel Robustness Computation for Temporal Logic
TLTk is a Python toolbox for computing robustness of Metric Temporal Logic (MTL) and Signal Temporal Logic (STL) specifications. It enables parallel robustness computation, making it well-suited for runtime verification and falsification-based testing of Cyber-Physical Systems.
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.