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 commitee for AAAI 23, HSCC 23, HSCC 22, NFM 23, NFM 22. I have chaired repeatability evaluation for HSCC 2021, HSCC 2020.






Updates

Tweets by bardhhoxha

Publications

Peer-reviewed papers and technical reports

    PhD Thesis

    1. Formal Requirements-Driven Analysis of Cyber Physical Systems (PDF)
      Bardh Hoxha
      Arizona State University, Tempe, AZ, August 2017

    Presentations, Posters and Demos

    1. Demo: System Testing with S-TaLiRo: Recent Functionality and Additions (PDF)
      Bardh Hoxha and Georgios Fainekos
      ACM/IEEE Hybrid Systems: Computation and Control [HSCC], Vienna, Austria, April 2016
    2. Pareto Front Exploration for Parametric Temporal Logic Specifications of Cyber-Physical Systems (PDF, Pres)
      Bardh Hoxha and Georgios Fainekos
      1st Workshop on Monitoring and Testing of Cyber-Physical Systems [MTCPS], Vienna, Austria, April 2016
    3. Planning in Dynamic Environments Through Temporal Logic Monitoring (PDF, Pres)
      Bardh Hoxha and Georgios Fainekos
      The Thirtieth AAAI Conference on Artificial Intelligence Workshop on Planning for Hybrid Systems Phoenix [AAAI PlanHS], Arizona, February 2016
    4. VISPEC: A graphical tool for easy elicitation of MTL requirements (PDF, TechRep, Pres)
      Bardh Hoxha, Nikolaos Mavridis, and Georgios Fainekos
      IEEE/RSJ International Conference on Intelligent Robots and Systems [IROS], Hamburg, Germany, September 2015
    5. Demo: S-TaLiRo: A tool for Testing and Verification for Hybrid Systems: Recent Functionality and Additions (PDF)
      Bardh Hoxha, Houssam Abbas, Adel Dokhanchi, and Georgios Fainekos
      ACM/IEEE Hybrid Systems: Computation and Control [HSCC], Berlin, Germany, April 2014
    6. [Poster] Metric Temporal Logic Falsification and Path Planning for Robotic Systems (PDF)
      Bardh Hoxha and Georgios Fainekos
      ACM/IEEE Hybrid Systems: Computation and Control [HSCC], Berlin, Germany, April 2014
    7. [Poster] Robustness-Guided Temporal Logic Testing for Stochastic Hybrid Systems (PDF)
      Houssam Abbas, Bardh Hoxha, Georgios Fainekos, Koichi Ueda
      ACM/IEEE Hybrid Systems: Computation and Control [HSCC], Berlin, Germany, April 2014
    8. [Poster] Conformance Testing as Falsification for Cyber-Physical Systems (PDF)
      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 2014

    Teaching

    Southern Illinois University, Carbondale, IL

    • CS 404: Autonomous Mobile Robots - Spring 2019 (Link)
      Instructor: Bardh Hoxha
    • CS 410/591: Computer Security - Spring 2019 (Link)
      Instructor: Bardh Hoxha
    • CS 491/591: Cyber-Physical Systems - Fall 2018 (Link)
      Instructor: Bardh Hoxha
    • CS 499: Senior Project - Spring 2018 (Link)
      Instructor: Bardh Hoxha
    • CS 498: Senior Project - Fall 2017 (Link)
      Instructor: Bardh Hoxha
    • CS 290: Comm Skills & Ethics - Fall 2017 (Link)
      Instructor: Bardh Hoxha

    Arizona State University, Tempe, AZ

    • CSE 552: Randomized and Approximation Algorithms - Fall 2013 (Link)
      Instructor: Charles Colbourn
      TA: Bardh Hoxha
    • CSE 355: Introduction to Theoretical Computer Science - Fall 2012 (Link)
      Instructor: Georgios Fainekos
      TA: Bardh Hoxha

    Central Connecticut State University, New Britain, CT

    • Algebra - 2011
      Instructor: Bardh Hoxha

    Capital Community College, Hartford, CT

    • Principles of Statistics - 2011
      Instructor: Bardh Hoxha
    • Introduction to Software Applications - 2011
      Instructor: Bardh Hoxha
    • Statway - 2011
      Instructor: Bardh Hoxha

    Software

    CBFKit: A Control Barrier Function Toolbox for Robotics Applications

    CBFKit is a Python/ROS2 toolbox designed to facilitate safe planning and control for robotics applications, particularly in uncertain environments. The toolbox utilizes Control Barrier Functions (CBFs) to provide formal safety guarantees while offering flexibility and ease of use. Key features include:
    • Generalized Framework: Supports the design of CBFs for various robotic systems operating in both deterministic and stochastic settings.
    • ROS Integration: Seamlessly connects with ROS2, enabling multi-robot applications, environment and map encoding, and integration with motion planning algorithms.
    • Diverse CBF Options: Provides a variety of CBF formulations and algorithms to address different control scenarios.
    • Model-based and Model-free Control: Accommodates both model-based control strategies using system dynamics and model-free control approaches.
    • Safety Guarantee: CBFs provide mathematically rigorous guarantees of safety by ensuring the system remains within a defined safe operating region.
    • Flexibility: Allows users to specify custom safety constraints and barrier functions to tailor the control behavior to specific needs.
    • Efficiency: Leverages JAX for efficient automatic differentiation and jaxopt for fast quadratic program (QP) solving, enabling real-time control applications.
    • Code Generation: Simplifies model creation with automatic code generation for dynamics, controllers, and certificate functions.
    • Usability: Includes tutorials and examples for a smooth learning curve and rapid prototyping.
    • Functional Programming: Built on functional programming principles, emphasizing data immutability and programmatic determinism.
    • The repository can be found here.

    Strem: A Spatio-Temporal Regular Expression Matcher

    STREM, implemented in RUST, is a versatile tool for efficient pattern matching in perception streams, suitable for both offline (design time) and online (operational time) use. Utilizing Spatial Regular Expressions (SpREs), it seamlessly combines classic Regular Expressions with advanced topological logic. This unique combination enables queries to detect occlusions and track object interactions over time. Strem's user-friendly interface is reminiscent of familiar RE tools like grep, yet it provides sophisticated spatial and temporal reasoning capabilities. Key features include:
    • Dual functionality for offline and online pattern matching.
    • Modular design compatible with Linux, Bash, and CLI tools, ideal for verification and validation processes.
    • Advanced RE × S4u querying language for precise matching in spatio-temporal data sequences.
    • Fast processing, thanks to efficient pattern matching algorithms.
    • Integration with LLM for Natural Language to SpRE Translation.
    • ROS Integration for enhanced robotics applications.
    • Demonstrations using the Woven Planet Perception AV dataset (offline) and integration with ROS and CARLA simulators (online).
    • The repository can be found here.

    Veritex: Deep Neural Network Verification

    Veritex is a Python toolbox for verification and automated repair of Deep Neural Networks. The tool enables:
    • Computation of exact or over-approximated output reachable sets
    • For usafe reachable sets, backtrack and find corresponding inputs for debugging
    • Plot 2 or 3-dimensional reachable domains
    • Automatically produce a provably safe DNN
    • Support well-known DNN formats such as ONNX and PyTorch
    • The repo can be found here.

    TLTk: Lightweight Tool for Robustness Computation of STL

    TLTk is a modular tool for parallel robustness computation of Signal Temporal Logic (STL) specifications. At the core of the tool, an algorithm for robustness computation is utilized that supports multi-threaded CPU/GPU computation. . The tool enables parallel robustness computation of large traces. In addition, the python implementation enables the addition and modification of temporal operators for application-specific scenarios
    • The user guide can be found here.
    • The docker image can be found here.
    • The repo can be found here.
    • The python library can be found here.

    S-TaLiRo: Toolbox for Testing and Verification of CPS

    S-TaLiro is a suite of tools for testing and verification of Cyber-Physical Systems. It is a toolbox for Matlab/Simulink. It enables the analysis of continuous and hybrid dynamical systems using temporal logics.
    The main features of S-TaLiRo include:
    • Robustness guided falsification of MTL specifications
    • Parameter estimation of parametric MTL formulas
    • Finding the expected robustness of Stochasic Systems
    • Runtime Verification of MTL specifications
    • Conformance testing
    S-TaLiRo has been applied to numerous challenging applications from the automotive and medical device industries. To download or learn more visit the S-TaLiRo website. The DIFTS2014 paper also provides a good overview of the tool and its features.
    In 2012 and 2014, S-Taliro was nominated as a technological breakthrough by the industry! (Read the report)

    ViSpec: Elicitation of Formal Specifications

    One of the main barriers preventing widespread use of formal methods is the elicitation of formal specifications. ViSpec is a graphical tool designed for the development and visualization of formal specifications by people that do not have training in formal logic. The tool enables users to develop specifications using a graphical formalism which is then automatically translated to Metric Temporal Logic (MTL). .
    Follow the link to download the software. Update coming soon...

    Contact

    Email: Mountain View
    LinkedIn: Link
    Google Scholar: Link
    Mathematics Genealogy: Link
    --- generated using this repo using data from the Mathematics Genealogy Project