Mountain View

Bardh Hoxha

Assistant Professor

Southern Illinois University

Bardh is an Assistant Professor in the Computer Department at Southern Illinois University. Previously, Bardh was part of the Cyber-Physical Systems Lab at Arizona State University. He has a PhD degree in Computer Science. He received his Masters degree in Mathematics from Central Connecticut State University and a Bachelors degree in Computer Science from New York Institute of Technology.

His main research interests include: Formal methods, Testing and Verification of Cyber-Physical Systems, Logic, Motion Planning for Autonomous Vehicles, and Human Robot Interaction.

Peer-reviewed papers and technical reports

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

Southern Illinois University, Carbondale, IL

  • 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
  • Instructor: Bardh Hoxha


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)


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...
Email: bhoxha at asu dot edu
LinkedIn: Link
Google Scholar: Link
Office Address: Centerpoint 203-12GA, 660 W 6th St, STE 203, Tempe, AZ 85281 (Google maps)

S5 & Summer of Innovation - Dayton, Ohio - Summer 2017

The summer of innovation event was organized by AFRL & WBI to apply formal methods to their UxAS multi-vehicle planning system.