Mountain View

Bardh Hoxha

PhD Candidate in Computer Science

Arizona State University

Bardh is a reserach assistant in the Cyber-Physical Systems Lab at Arizona State University. He is a PhD candidate 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

  1. Mining parametric temporal logic properties in model-based design for cyber-physical systems (PDF, Extended tech report PDF)
    Bardh Hoxha, Adel Dokhanchi and Georgios Fainekos
    International Journal on Software Tools for Technology Transfer [STTT], 2017
  2. An Efficient Algorithm for Monitoring Practical TPTL Specifications (PDF)
    Adel Dokhanchi, Bardh Hoxha, Cumhur Erkan Tuncali, and Georgios Fainekos
    The 14th ACM-IEEE International Conference on Formal Methods and Models for System Design [MEMOCODE], Kanpur, India, November 2016
  3. Pareto Front Exploration for Parametric Temporal Logic Specifications of Cyber-Physical Systems (PDF)
    Bardh Hoxha and Georgios Fainekos
    1st Workshop on Monitoring and Testing of Cyber-Physical Systems [MTCPS], Vienna, Austria, April 2016
  4. MITL Specification Debugging for Monitoring of Cyber-Physical Systems (PDF)
    Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos
    1st Workshop on Monitoring and Testing of Cyber-Physical Systems [MTCPS], Vienna, Austria, April 2016
  5. Planning in Dynamic Environments Through Temporal Logic Monitoring (PDF)
    Bardh Hoxha and Georgios Fainekos
    The Thirtieth AAAI Conference on Artificial Intelligence Workshop on Planning for Hybrid Systems [AAAI PlanHS], Phoenix, Arizona, February 2016
  6. Metric Interval Temporal Logic Specification Elicitation and Debugging (PDF)
    Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos
    The 13th ACM-IEEE International Conference on Formal Methods and Models for System Design [MEMOCODE], Austin, Texas, September 2015
  7. VISPEC: A graphical tool for elicitation of MTL requirements (PDF, TechRep)
    Bardh Hoxha, Nikolaos Mavridis, and Georgios Fainekos
    IEEE/RSJ International Conference on Intelligent Robots and Systems [IROS], Hamburg, Germany, September 2015
  8. Towards Formal Specification Visualization for Testing and Monitoring of Cyber-Physical Systems (PDF)
    Bardh Hoxha, Hoang Bach, Houssam Abbas, Adel Dokhanchi, Yoshihiro Kobayashi, and Georgios Fainekos
    Design and Implementation of Formal Tools and Systems [DIFTS], Lausanne, Switzerland, October 2014
  9. On-Line Monitoring for Temporal Logic Robustness (PDF)
    Adel Dokhanchi, Bardh Hoxha and Georgios Fainekos,
    Runtime Verification [RV], Toronto, Canada, September 2014
  10. Conformance Testing as Falsification for Cyber-Physical Systems (PDF)
    H. Abbas, B. Hoxha, G. Fainekos, J. V. Deshmukh, J. Kapinski, K. Ueda
    Technical Report arXiv:1401.5200, 2014
  11. WiP Abstract: 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
  12. Robustness-Guided Temporal Logic Testing and Verification for Stochastic Cyber-Physical Systems★ (PDF)
    Houssam Abbas*, Bardh Hoxha*, Georgios Fainekos, Koichi Ueda
    IEEE International Conference on CYBER Technology in Automation, Control, and Intelligent Systems [CYBER], Hong Kong, June 2014
    * Authors contributed equally to the work.
    ★ Finalist for best student paper award
  13. Benchmarks for Temporal Logic Requirements for Automotive Systems (PDF)
    Bardh Hoxha, Houssam Abbas and Georgios Fainekos
    Applied Verification for Continuous and Hybrid Systems [ARCH], Berlin, Germany, April 2014
  14. Using S-TaLiRo on Industrial Size Automotive Models (PDF)
    Bardh Hoxha, Houssam Abbas and Georgios Fainekos
    Applied Verification for Continuous and Hybrid Systems [ARCH], Berlin, Germany, April 2014
  15. Querying Parametric Temporal Logic Properties on Embedded Systems (PDF)
    Hengyi Yang, Bardh Hoxha and Georgios Fainekos
    Int. Conference on Testing Software and Systems [ICTSS], Aalborg, Denmark, Nov. 2012

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

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

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