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
Peer-reviewed Papers and Technical Reports
PhD Thesis
Formal Requirements-Driven Analysis of Cyber Physical Systems
Bardh Hoxha
Arizona State University, Tempe, AZ, August 2017
PDFPresentations, Posters and Demos
Demo: System Testing with S-TaLiRo: Recent Functionality and Additions
Bardh Hoxha and Georgios Fainekos
ACM/IEEE Hybrid Systems: Computation and Control [HSCC], Vienna, Austria, April 2016
PDFTeaching
Southern Illinois University, Carbondale, IL
CS 404: Autonomous Mobile Robots
Spring 2019Instructor: Bardh Hoxha
CS 410/591: Computer Security
Spring 2019Instructor: Bardh Hoxha
CS 491/591: Cyber-Physical Systems
Fall 2018Instructor: Bardh Hoxha
CS 499: Senior Project
Spring 2018Instructor: Bardh Hoxha
CS 498: Senior Project
Fall 2017Instructor: Bardh Hoxha
CS 290: Communication Skills & Ethics
Fall 2017Instructor: Bardh Hoxha
Arizona State University, Tempe, AZ
CSE 552: Randomized and Approximation Algorithms
Fall 2013Instructor: Charles Colbourn | TA: Bardh Hoxha
Course LinkCSE 355: Introduction to Theoretical Computer Science
Fall 2012Instructor: Georgios Fainekos | TA: Bardh Hoxha
Course LinkSoftware
CBFKit: A Control Barrier Function Toolbox for Robotics Applications
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, ensuring safety even in uncertain environments.
Repository ... IROS2024STREM: A Spatio-Temporal Regular Expression Matcher
STREM, written in RUST, is a flexible tool for efficient pattern matching in perception streams, supporting both offline and online use. It employs Spatial Regular Expressions (SpREs), merging classic regex with topological logic to enable queries for occlusions and object interactions over time. Its interface, similar to grep, offers advanced spatial and temporal reasoning.
Repository ... STTT2024NDF-CoRoCo: Cooperative Perception with Neural Density Fields
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.
RTAMT: Real-Time STL Monitoring Library
RTAMT is a Python library for real-time and offline monitoring of Signal Temporal Logic (STL) specifications. It supports both discrete-time and dense-time semantics, with optimized performance for online applications.
- Offline & Online STL Monitoring
- Discrete-Time & Dense-Time Support
- Optimized C++ Backend for Online Monitoring
- Python 2 and 3 Compatible
StarV: Event-driven Monitoring & Verification Codesign
StarV is a framework for monitoring and verification codesign in distributed learning-enabled Cyber-Physical Systems. It uses event-driven execution and star set reachability to verify complex behaviors of dynamical systems in real time.
- Event-driven Monitoring Architecture
- Supports Distributed CPS with Learning Components
- Star Set-based Reachability Analysis
- Focus on Real-time Safety and Efficiency
Specless: SPECification LEarning and Strategy Synthesis
Python library for learning specification from demonstrations and synthesizing strategies that satisfy the given specification. Can be used in various applications including task assignment for robotics.
MRTA-sim: Multi-Robot Task Allocation Stack
A ROS package providing a stack for simulating and implementing various multi-robot task allocation (MRTA) algorithms in environments like Gazebo.
SMrTa: SMT-Based Dynamic Multi-Robot Task Allocation
Implementation for the NFM 2024 paper "SMT-Based Dynamic Multi-Robot Task Allocation", providing tools for solving dynamic MRTA problems using SMT solvers.
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. It helps debug unsafe behaviors and generate provably safe DNNs.
Repository ...TLTk: Lightweight Tool for Robustness Computation of STL
TLTk is a modular Python-based tool for parallel robustness computation of Signal Temporal Logic (STL) specifications. It supports multi-threaded CPU/GPU execution and enables extensible operator definitions.
User Guide Docker Bitbucket PyPIS-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.
Website DIFTS2014 NSF ReportViSpec: Elicitation of Formal Specifications
ViSpec is a graphical tool designed to help non-experts develop formal specifications using an intuitive interface. It translates visual representations into Metric Temporal Logic (MTL) automatically.
- Visual MTL Specification Builder
- Automatic Translation to Formal Logic
- Accessible to Users Without Formal Methods Expertise
Contact
-
Email:
- LinkedIn: linkedin.com/in/bardhhoxha
- Google Scholar: View Profile
-
Mathematics Genealogy:
View Tree (PDF)
--- Generated using this repo & data from the Math Genealogy Project.