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

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

    Veritex

    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

    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

    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

    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