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
PDFPresentations, 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
PDFResearch Areas
Safe Learning-Based Control
Control Theory + Machine LearningControl methods that integrate learning algorithms with formal safety constraints for autonomous system behavior.
Research Focus:
- • Mathematical frameworks for safety during learning
- • Real-time constraint satisfaction in uncertain environments
- • Applications in robotics and autonomous navigation
Runtime Verification & Monitoring
Real-time Safety AssuranceReal-time monitoring systems for system safety and correctness during operation using formal specification languages.
Research Focus:
- • Online monitoring algorithms with low overhead
- • Distributed monitoring for multi-agent systems
- • Event-driven architectures for scalability
System Testing & Falsification
Automated VerificationAutomated testing frameworks for finding system failures and validating cyber-physical systems against temporal logic specifications.
Research Focus:
- • Search-based testing using evolutionary algorithms
- • Robustness analysis and quantification
- • Simulation-based verification approaches
Autonomous Systems
Multi-Agent SystemsAutonomous system design with focus on safety, reliability, and performance in complex environments.
Research Focus:
- • Cooperative perception and decision making
- • Task assignment and scheduling
- • Human-robot interaction
Spatial-Temporal Reasoning
Pattern Recognition & LogicPattern matching and reasoning over spatial and temporal data streams using logical frameworks and algorithms.
Research Focus:
- • Spatial Regular Expressions for object interactions
- • Real-time pattern matching in perception streams
- • Topological reasoning about occlusions and visibility
Risk & Uncertainty
Probabilistic SafetyHandling uncertainty and risk in safety-critical systems through probabilistic and stochastic methods.
Research Focus:
- • Probabilistic safety analysis with confidence bounds
- • Stochastic reachability for uncertain systems
- • Risk-aware planning and decision making
Teaching
I am passionate about education and have taught a diverse range of courses in computer science, focusing on both theoretical foundations and practical applications in autonomous systems and cybersecurity.
Southern Illinois University, Carbondale, IL
Course Description: Advanced undergraduate course covering the fundamentals of autonomous mobile robotics including sensing, perception, localization, mapping, path planning, and control.
Topics Covered:
- Robot kinematics and dynamics
- Sensor fusion and perception
- SLAM (Simultaneous Localization and Mapping)
- Path planning algorithms
- Control theory for mobile robots
- ROS (Robot Operating System) programming
Projects: Students implemented autonomous navigation systems using real mobile robots and simulation environments.
Course Description: Comprehensive course on computer security principles, practices, and applications for both undergraduate and graduate students.
Topics Covered:
- Cryptography and encryption methods
- Network security protocols
- System vulnerabilities and attack vectors
- Access control and authentication
- Security in cyber-physical systems
- Incident response and forensics
Hands-on Labs: Students gained practical experience with penetration testing, cryptographic implementations, and security analysis tools.
Course Description: Advanced course introducing the design, analysis, and verification of cyber-physical systems that integrate computation, networking, and physical processes.
Topics Covered:
- Hybrid system modeling and analysis
- Real-time systems and scheduling
- Formal verification methods
- Temporal logic specifications
- Control theory for CPS
- Safety and security in CPS
Research Component: Graduate students conducted original research projects in CPS verification and published results in workshop proceedings.
Course Description: Capstone project course where students work individually or in teams to design, implement, and present substantial software systems.
Project Examples:
- Autonomous drone navigation system
- IoT-based smart home security platform
- Machine learning-based medical diagnosis tool
- Real-time traffic monitoring system
Skills Developed: Project management, software engineering practices, technical presentation, and real-world problem solving.
Course Description: First semester of the two-semester senior capstone sequence, focusing on project planning, requirements analysis, and initial implementation.
Learning Outcomes:
- Requirements engineering and system design
- Technology selection and architecture planning
- Project timeline and milestone development
- Literature review and market analysis
Course Description: Essential course developing professional communication skills and understanding of ethical issues in computer science and technology.
Key Components:
- Technical writing and documentation
- Oral presentation skills
- Professional ethics in computing
- Privacy and data protection
- Social responsibility in technology
- Team collaboration and leadership
Assessment Methods: Technical reports, presentations, case study analyses, and peer evaluations.
Arizona State University, Tempe, AZ
CSE 552: Randomized and Approximation Algorithms
Fall 2013Instructor: Charles Colbourn | TA: Bardh Hoxha
Graduate-level course covering probabilistic algorithms, randomized data structures, approximation algorithms, and their applications in computer science and optimization.
Course LinkCSE 355: Introduction to Theoretical Computer Science
Fall 2012Instructor: Georgios Fainekos | TA: Bardh Hoxha
Fundamental course covering automata theory, formal languages, computability, and complexity theory, providing the theoretical foundation for computer science.
Course LinkTeaching Philosophy
My teaching approach integrates theoretical foundations with practical applications to prepare students for complex challenges in computer science and engineering. I focus on:
- Project-Based Learning: Connecting theoretical concepts to real implementations
- Problem-Solving Skills: Developing systematic approaches to complex problems
- Current Technologies: Using industry-standard tools and methods
- Technical Communication: Emphasizing clear documentation and presentation
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 ... IROS2024STREM: 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 ... STTT2024NDF-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
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
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 PyPIS-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 ReportViSpec: 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
-
Email:
- LinkedIn: linkedin.com/in/bardhhoxha
- Google Scholar: View Profile
-
Mathematics Genealogy:
View Tree (PDF)
--- Generated using this repo & data from the Math Genealogy Project.