I’m Huan Zhang, a Ph.D. candidate in Computer Science at Maynooth University, specializing in formal verification for autonomous robotic systems. My research addresses a critical gap in autonomous system deployment: formal verification is typically offline, but deployed systems evolve.

I develop VeriROS, a framework that brings offline verification guarantees into runtime execution using machine-checkable certificates and SMT-based reasoning. This enables autonomous systems to remain provably safe even after code or configuration changes—critical for real-world robot deployment.

Research focus: Bridging formal verification (model checking, SMT solving) with practical ROS2 execution through runtime monitoring and dynamic response policies.

News

2026.04: Paper “Verifying an Elevator Scheduling Control System” accepted at ITEQS@ICST 2026.
2026.01: Paper “VeriROS: Verifiable ROS2 Navigation Execution Framework” accepted at FormaliSE 2026.
2025.09: Poster presentation at Swiss CLOCK Summit.
2025.08: Attended VeTSS (Verification Teaching Summer School).
2025.07: Attended OPLSS (Oregon Programming Languages Summer School).
2023.12: Integrated model-checking framework with ROS in VeriROS.

Publications

Verifying an Elevator Scheduling Control System — Huan Zhang et al., ITEQS@ICST 2026 (accepted)
VeriROS: Verifiable ROS2 Navigation Execution Framework — Huan Zhang et al., FormaliSE 2026 (accepted) [View Paper]
Challenges in Autonomous Robotic System Verification — Huan Zhang, Hao Wu, CEUR Workshop Proceedings, Vol. 3860 [View Paper]
Improving Semi-Supervised Image Classification by Assigning Different Weights — Huan Zhang et al., Applied Sciences, Vol. 12(3) [View Paper]

Educations

Ph.D. in Computer Science, Maynooth University, Ireland (2023–Present)
Formal Verification of Autonomous Robotic Systems
MSc in Computer Science, Newcastle University, UK (2022–2023) – Distinction
BSc in Robotics Engineering, Beijing Institute of Technology, Zhuhai (2017–2021) – First Class Honours