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
Showing 76 publications
76
Quantitative Verification of Learning-Enabled Systems using ProbStar Reachability
Yuntao Li, Sung Woo Choi, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos, Hoang-Dung Tran
Nonlinear Analysis: Hybrid Systems 20262026
journal PDF
75
FiReFly: Fair Distributed Receding Horizon Planning for Multiple UAVs
Nathan Fronda, Bardh Hoxha, Houssam Abbas
IEEE Intelligent Transportation Systems Conference (ITSC), 20262026
conference PDF
74
Fair-CoPlan: Negotiated Flight Planning with Fair Deconfliction for Urban Air Mobility
Nathan Fronda, Peter Smith, Bardh Hoxha, Yash Pant, Houssam Abbas
IEEE Intelligent Transportation Systems Conference (ITSC), 20262026
conference PDF
73
Scalable Multi-Agent Path Finding for Delivery Robot Systems with Temporal and Edge Capacity Constraints on Weighted Graphs
Tomoya Yamaguchi, Ippei Nishitani, Yusuke Ota, Bardh Hoxha, Georgios Fainekos
2025 IEEE 21st International Conference on Automation Science and Engineering (CASE), 20252025
conference PDF
72
GPU-Accelerated Barrier-Rate Guided MPPI Control for Tractor-Trailer Systems
Keyvan Majd, Hardik Parwana, Bardh Hoxha, Steven Hong, Hideki Okamoto, Georgios Fainekos
arXiv preprint arXiv:2508.05773, 20252025
conference PDF
71
STL-GO: Spatio-Temporal Logic with Graph Operators for Distributed Systems with Multiple Network Topologies
Yiqi Zhao, Xinyi Yu, Bardh Hoxha, Georgios Fainekos, Jyotirmoy Deshmukh, Lars Lindemann
ACM Transactions on Embedded Computing Systems (TECS), 20252025
journal PDF
70
Conformal Prediction in the Loop: Risk-Aware Control Barrier Functions for Stochastic Systems with Data-Driven State Estimators
Jiaqi Zhang, Bardh Hoxha, Georgios Fainekos, Dimitra Panagou
IEEE Control Systems Letters, 20252025
journal PDF
69
ProbStar Temporal Logic for Verifying Complex Behaviors of Learning-enabled Systems
Hoang-Dung Tran, Sung Woo Choi, Yuntao Li, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos
28th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 20252025
conference PDF
68
BR-MPPI: Barrier Rate guided MPPI for Enforcing Multiple Inequality Constraints with Learned Signed Distance Field
Hardik Parwana, Taekyung Kim, Kehan Long, Bardh Hoxha, Hideki Okamoto, Georgios Fainekos, Dimitra Panagou
arXiv:2506.07325, 20252025
conference PDF
67
StarV: A Qualitative and Quantitative Verification Tool for Learning-Enabled Systems
Hoang-Dung Tran, Sung Woo Choi, Yuntao Li, Qing Liu, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos
International Conference on Computer Aided Verification (CAV), 20252025
conference PDF
66
Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications
Yiqi Zhao, Emily Zhu, Bardh Hoxha, Georgios Fainekos, Jyotirmoy V Deshmukh, Lars Lindemann
Transactions on Cyber-Physical Systems (TCPS), 20252025
journal PDF
65
Safe Navigation in Uncertain Crowded Environments Using Risk Adaptive CVaR Barrier Functions
Xinyi Wang, Taekyung Kim, Bardh Hoxha, Georgios Fainekos, Dimitra Panagou
arXiv preprint arXiv:2504.06513, 20252025
conference PDF
64
Reachability Analysis of Recurrent Neural Networks
Sung Woo Choi, Yuntao Li, Xiaodong Yang, Tomoya Yamaguchi, Bardh Hoxha, Georgios Fainekos, Danil Prokhorov, Hoang-Dung Tran
Nonlinear Analysis: Hybrid Systems, 20252025
journal PDF
63
Scaling Learning-based Policy Optimization for Temporal Logic Tasks by Controller Network Dropout
Navid Hashemi, Bardh Hoxha, Danil Prokhorov, Georgios Fainekos, Jyotirmoy V Deshmukh
Transactions on Cyber-Physical Systems, 20252025
journal PDF
61
MRTA-Sim: A Modular Simulator for Multi-Robot Allocation, Planning, and Control in Open-World Environments
Victoria Marie Tuck, Hardik Parwana, Pei-Wei Chen, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, S Shankar Sastry, Sanjit A Seshia
arXiv, 20252025
conference PDF
60
From Dashcam Videos to Driving Simulations: Stress Testing Automated Vehicles Against Rare Events
Yan Miao, Georgios Fainekos, Bardh Hoxha, Hideki Okamoto, Danil Prokhorov, Sayan Mitra
Machine Learning for Autonomous Driving - AAAI, 20252025
conference PDF
56
Scaling Learning-based Policy Optimization for Temporal Logic Tasks by Controller Network Dropout
Navid Hashemi, Bardh Hoxha, Danil Prokhorov, Georgios Fainekos, Jyotirmoy Deshmukh
ACM Transactions on Cyber-Physical Systems, 20242024
journal PDF
55
LB4TL: Smooth Semantics for Temporal Logic for Scalable Training of Neural Feedback Controllers
Navid Hashemi, Sam Williams, Bardh Hoxha, Danil Prokhorov, Georgios Fainekos, Jyotirmoy Deshmukh
The 8th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS), July 20242024
conference PDF
52
Risk-Aware Fixed-Time Stabilization of Stochastic Systems under Measurement Uncertainty
Mitchell Black, Georgios Fainekos, Bardh Hoxha, Dimitra Panagou
American Control Conference (ACC), 20242024
conference PDF
50
Safe Control Synthesis for Hybrid Systems through Local Control Barrier Functions
Yang, Shuo, Black, Mitchell, Fainekos, Georgios, Hoxha, Bardh, Okamoto, Hideki, Mangharam, Rahul
2023
journal PDF
49
Robust Conformal Prediction for STL Runtime Verification under Distribution Shift
Zhao, Yiqi, Hoxha, Bardh, Fainekos, Georgios, Deshmukh, Jyotirmoy V, Lindemann, Lars
2023
Finalist for Best Paper Award
journal PDF
48
Feasible Space Monitoring for Multiple Control Barrier Functions with application to Large Scale Indoor Navigation
Parwana, Hardik, Black, Mitchell, Hoxha, Bardh, Okamoto, Hideki, Fainekos, Georgios, Prokhorov, Danil, Panagou, Dimitra
2023
journal PDF
45
Checkmate: Fault Timing Localization for Multi-Robot Scenarios
Nishitani, Ippei, Yamaguchi, Tomoya, Hoxha, Bardh
2023 IEEE 19th International Conference on Automation Science and Engineering (CASE)2023
conference PDF
42
A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems
Navid Hashemi, Bardh Hoxha, Tomoya Yamaguchi, Danil Prokhorov, Geogios Fainekos, Jyotirmoy Deshmukh
ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), 20232023
conference PDF
41
Risk-awareness in learning neural controllers for temporal logic objectives
Hashemi, Navid, Qin, Xin, Deshmukh, Jyotirmoy V, Fainekos, Georgios, Hoxha, Bardh, Prokhorov, Danil, Yamaguchi, Tomoya
2023 American Control Conference (ACC)2023
conference PDF
39
Safety Under Uncertainty: Tight Bounds with Risk-Aware Control Barrier Functions
Black, Mitchell, Fainekos, Georgios, Hoxha, Bardh, Prokhorov, Danil, Panagou, Dimitra
2023
journal PDF
38
Safety Verification and Repair of Deep Neural Networks
Xiaodong Yang, Tomoya Yamaguchi, Bardh Hoxha, Danil Prokhorov, Taylor T Johnson
Workshop on Formal Verification of Machine Learning (WFVML), 20222022
workshop PDF
37
Runtime Assurance for Autonomous Driving with Neural Reachability
Bogomolov, Sergiy, Hekal, Abdelrahman, Hoxha, Bardh, Yamaguchi, Tomoya
2022 IEEE 25th International Conference on Intelligent Transportation Systems (ITSC)2022
conference PDF
35
Formalizing and Evaluating Requirements of Perception Systems for Automated Vehicles using Spatio-Temporal Perception Logic
Hekmatnejad, Mohammad, Hoxha, Bardh, Deshmukh, Jyotirmoy V, Yang, Yezhou, Fainekos, Georgios
2022
journal PDF
34
Discovering physical interaction vulnerabilities in IoT deployments
Ozmen, Muslum Ozgur, Li, Xuansong, Chu, Andrew Chun-An, Celik, Z Berkay, Hoxha, Bardh, Zhang, Xiangyu
2021
journal PDF
33
Risk-bounded control with kalman filtering and stochastic barrier functions
Yaghoubi, Shakiba, Fainekos, Georgios, Yamaguchi, Tomoya, Prokhorov, Danil, Hoxha, Bardh
2021 60th IEEE Conference on Decision and Control (CDC)2021
conference PDF
31
Safe navigation in human occupied environments using sampling and control barrier functions
Majd, Keyvan, Yaghoubi, Shakiba, Yamaguchi, Tomoya, Hoxha, Bardh, Prokhorov, Danil, Fainekos, Georgios
2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)2021
conference PDF
29
Risk-bounded control using stochastic barrier functions
Yaghoubi, Shakiba, Majd, Keyvan, Fainekos, Georgios, Yamaguchi, Tomoya, Prokhorov, Danil, Hoxha, Bardh
2020
journal PDF
28
Search-based test-case generation by monitoring responsibility safety rules
Hekmatnejad, Mohammad, Hoxha, Bardh, Fainekos, Georgios
2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC)2020
conference PDF
27
Specification-guided software fault localization for autonomous mobile systems
Yamaguchi, Tomoya, Hoxha, Bardh, Prokhorov, Danil, Deshmukh, Jyotirmoy V
2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)2020
conference PDF
26
Application of Simulation-Based Methods on Autonomous Vehicle Control with Deep Neural Network: Work-in-Progress
Date, Yuji, Baba, Takeshi, Hoxha, Bardh, Yamaguchi, Tomoya, Prokhorov, Danil
2020 International Conference on Embedded Software (EMSOFT)2020
conference PDF
24
Robustness of specifications and its applications to falsification, parameter mining, and runtime monitoring with s-taliro
Fainekos, Georgios, Hoxha, Bardh, Sankaranarayanan, Sriram
Runtime Verification: 19th International Conference, RV 2019, Porto, Portugal, October 8--11, 2019, Proceedings 192019
23
Experience report: Application of falsification methods on the UxAS system
Tuncali, Cumhur Erkan, Hoxha, Bardh, Ding, Guohui, Fainekos, Georgios, Sankaranarayanan, Sriram
NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings 102018
conference PDF
22
Mission planning for multiple vehicles with temporal specifications using UxAS
Nguyen, Luan V, Hoxha, Bardh, Johnson, Taylor T, Fainekos, Georgios
2018
journal PDF
21
Formal requirement debugging for testing and verification of cyber-physical systems
Dokhanchi, Adel, Hoxha, Bardh, Fainekos, Georgios
2017
journal PDF
20
Vacuity aware falsification for MTL request-response specifications
Dokhanchi, Adel, Yaghoubi, Shakiba, Hoxha, Bardh, Fainekos, Georgios
2017 13th IEEE Conference on Automation Science and Engineering (CASE)2017
conference PDF
19
Mining parametric temporal logic properties in model-based design for cyber-physical systems
Hoxha, Bardh, Dokhanchi, Adel, Fainekos, Georgios
2017
journal PDF
18
An efficient algorithm for monitoring practical TPTL specifications
Dokhanchi, Adel, Hoxha, Bardh, Tuncali, Cumhur Erkan, Fainekos, Georgios
2016 ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)2016
conference PDF
17
Pareto front exploration for parametric temporal logic specifications of cyber-physical systems
Hoxha, Bardh, Fainekos, Georgios
Workshop on Monitoring and Testing of Cyber-Physical Systems2016
workshop PDF
16
MITL specification debugging for monitoring of cyber-physical systems
Dokhanchi, Adel, Hoxha, Bardh, Fainekos, Georgios
2016
journal PDF
15
Planning in Dynamic Environments Through Temporal Logic Monitoring
Hoxha, Bardh, Fainekos, Georgios
AAAI Workshop: Planning for Hybrid Systems2016
workshop PDF
14
Metric interval temporal logic specification elicitation and debugging
Dokhanchi, Adel, Hoxha, Bardh, Fainekos, Georgios
2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)2015
conference PDF
13
VISPEC: A graphical tool for elicitation of MTL requirements
Hoxha, Bardh, Mavridis, Nikolaos, Fainekos, Georgios
2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)2015
conference PDF
12
Towards formal specification visualization for testing and monitoring of cyber-physical systems
Hoxha, Bardh, Bach, Hoang, Abbas, Houssam, Dokhanchi, Adel, Kobayashi, Yoshihiro, Fainekos, Georgios
Int. Workshop on Design and Implementation of Formal Tools and Systems2014
workshop PDF
11
On-line monitoring for temporal logic robustness
Dokhanchi, Adel, Hoxha, Bardh, Fainekos, Georgios
International Conference on Runtime Verification2014
conference PDF
10
Conformance testing as falsification for cyber-physical systems
Abbas, Houssam, Hoxha, Bardh, Fainekos, Georgios, Deshmukh, Jyotirmoy V, Kapinski, James, Ueda, Koichi
2014
journal PDF
9
WiP Abstract: Conformance Testing as Falsification for Cyber-Physical Systems
H. Abbas, B. Hoxha, G. Fainekos, J. V. Deshmukh, J. Kapinski, K. Ueda
ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), Berlin, Germany, April 20142014
conference PDF
8
Robustness-guided temporal logic testing and verification for stochastic cyber-physical systems
Abbas, Houssam, Hoxha, Bardh, Fainekos, Georgios, Ueda, Koichi
The 4th Annual IEEE International Conference on Cyber Technology in Automation, Control and Intelligent2014
Finalist for best student paper award
conference PDF
7
Using S-TaLiRo on industrial size automotive models
Hoxha, Bardh, Abbas, Houssam, Fainekos, Georgios
2014
journal PDF
6
Querying parametric temporal logic properties on embedded systems
Yang, Hengyi, Hoxha, Bardh, Fainekos, Georgios
IFIP International Conference on Testing Software and Systems2012
conference PDF
4
ARCH-COMP18 Category Report: Results on the Falsification Benchmarks
Dokhanchi, Adel, Yaghoubi, Shakiba, Hoxha, Bardh, Fainekos, Georgios, Ernst, Gidon, Zhang, Zhenya, Arcaini, Paolo, Hasuo, Ichiro, Sedwards, Sean
ARCH
conference PDF
3
ARCH-COMP17 Category Report: Preliminary Results on the Falsification Benchmarks
Dokhanchi, Adel, Yaghoubi, Shakiba, Hoxha, Bardh, Fainekos, Georgios
ARCH
conference PDF
2
Benchmarks for Temporal Logic Requirements for Automotive Systems
Hoxha, Bardh, Abbas, Houssam, Fainekos, Georgios
journal PDF
1
System Testing with S-TaLiRo: Recent Functionality and Additions
Hoxha, Bardh, Dokhanchi, Adel, Fainekos, Georgios
journal PDF
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.
Control Barrier FunctionsNeural LyapunovSafe RL
Autonomous Systems
Multi-Agent Systems
Designing algorithms for coordination, planning, and control of multiple autonomous agents in complex, dynamic environments.
Multi-Robot PlanningDecentralized ControlSwarm Robotics
Formal Methods
Verification & Synthesis
Applying rigorous mathematical techniques to specify, develop, and verify software and hardware systems.
Temporal LogicReachability AnalysisFalsification
Runtime Monitoring
System Health & Safety
Techniques for observing system behavior during execution to detect violations of safety properties or performance requirements.
Signal Temporal LogicOnline VerificationPredictive Monitoring
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.
OfficeToyota Research Institute of North America
1555 Woodridge Ave
Ann Arbor, MI 48105
1555 Woodridge Ave
Ann Arbor, MI 48105