Building Safer Autonomous Systems
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
LogSTOP: Temporal Scores over Prediction Sequences for Matching and Retrieval
Temporal Specification Guidance for Text-to-Video Generation
Safety-aware Model Predictive Path Integral Control with Signal Temporal Logic
Diffusion-Guided Search via Exponential Tilting (DiffTilt): An Application to Falsification of Safety-Critical Systems
FalconTrack: Photorealistic Auto-Labeled Perception and Physics-Aware Vision-Based Aerial Tracking
Sample-Efficient Learning of Probabilistic Causes for Reachability in Markov Decision Processes with Probabilistic Guarantees
DiffCVaR: 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
Safe Model Predictive Diffusion with Shielding
Performance-Guided Refinement for Visual Aerial Navigation using Editable Gaussian Splatting in FalconGym 2.0
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
Patents
Learning abstractions for multi-robot path planning in unstructured environments
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
Neural configuration distance function for continuum robot control
Methods of qualitative and quantitative verification of complex learning-enabled systems and temporal logic verification
System and method for manipulating an omnidirectional cart using an armed robot
Producing a simulation recording to test an automated driving system
Methods and systems for spatio-temporal regular expression matching
System and method for optimization of vehicle perception sensor configuration
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
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.
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.
STREM: Spatio-Temporal Pattern Matching over Perception Streams
STREM is a Rust command-line tool that matches spatio-temporal patterns against annotated perception streams. Using Spatial Regular Expressions (SpREs), it combines regular-expression-style temporal patterns with spatial reasoning over bounding-box detections, making it possible to query large video and autonomous driving datasets for specific scenarios.
RTAMT: Runtime Robustness Monitors for STL
RTAMT is a Python library for monitoring Signal Temporal Logic (STL) specifications. It supports offline and online (real-time) monitoring with both discrete- and dense-time semantics and quantitative robustness degrees, making it well-suited for runtime verification of Cyber-Physical Systems and robotics.
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.