Bardh Hoxha Profile Picture

Bardh Hoxha

Senior Principal Scientist

Toyota Research Institute of North America (TRINA)

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

PDF

Presentations, 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

PDF
Pareto Front Exploration for Parametric Temporal Logic Specifications of Cyber-Physical Systems
Bardh Hoxha and Georgios Fainekos

1st Workshop on Monitoring and Testing of Cyber-Physical Systems [MTCPS], Vienna, Austria, April 2016

PDF Pres

Teaching

Southern Illinois University, Carbondale, IL

Arizona State University, Tempe, AZ

CSE 552: Randomized and Approximation Algorithms
Fall 2013

Instructor: Charles Colbourn | TA: Bardh Hoxha

Course Link
CSE 355: Introduction to Theoretical Computer Science
Fall 2012

Instructor: Georgios Fainekos | TA: Bardh Hoxha

Course Link

Software

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 ... IROS2024

STREM: 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 ... STTT2024

NDF-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
Repository ... STTT2023

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
Repository ...

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 PyPI

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.

Website DIFTS2014 NSF Report

ViSpec: 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