Verification and Validation for Learning-enabled Autonomy

Hoang-Dung Tran

University of Florida

Department of Computer and Information Science and Engineering (CISE)

Research Interests: Formal Methods, Safe AI, Cyber-Physical Systems, Robotics, Control

Bio: I am an Assistant Professor in the Department of Computer and Information Science and Engineering (CISE) at the University of Florida. I earned a Ph.D. degree in Computer Science at Vanderbilt University in August 2020. My research interests are reachability analysis and robustness certification of deep neural networks (DNN), formal verification of autonomous cyber-physical systems(CPS) with learning-enabled components, safe and robust training for DNN, real-time verification, and safe motion planning for distributed CPS. I am also interested in robust control, stability analysis of nonlinear control systems, and networked control systems.

Hiring: I am seeking two PhD students to join my group at UF CISE, working on Formal Methods for deep learning models, learning-enabled autonomy, and Causal Reinforcement Learning. Students with a Master's Degree in CS/ECE with a strong research background in formal verification, robotics, reinforcement learning, and control are welcome to apply. I am particularly looking for students with the following backgrounds:

Having a Master's Degree (in the US is prefered)
Publishing papers as first author in formal methods, cyber-physical systems, machine learning, robotics, and control conferences, such as:
- Formal methods and CPS: NFM, CAV, HSCC, ICCPS, FM, EMSOFT, TACAS, etc.
- Machine learning: Neurips, ICML, ICLR, AAAI
- Robotics: RSS, ICRA, IROS, CoRL
- Control: ACC, CDC

If you are interested, please send your CV to dungtran@ufl.edu. Note: I only reply to emails from potential applicants.

Google Scholar, ResearchGate

Research

I am leading the research and development of the following projects and tools.

NNV: Verification for Deep Neural Networks and Learning-enabled Cyber-Physical Systems
StarV: A Qualitative and Quantitative Verification Tool for Deep Neural Networks and Complex Learning-enabled Autonomy
DLe-CPS: Indoor Learning-based Distributed Autonomous Driving Testbed
SHRC: Safe Human-Robot-Collaboration
DRREACH: Decentralized Realtime Verification and Safe Motion Planning for Distributed Autonomous Cyber-Physical Systems
DAEV: Reachability Analysis, Verification, and Falsification for High-Index Differential Algebraic Equations
PDEV: Reachability Analysis, Verification, and Falsification for Partial Differential Equations

Awards

NSF CAREER, 2025
SIU PRIZE (Gold Medal) for Young Vietnamese Researchers Worldwide in Computer Science, 2025.
UNL College of Engineering Research Excellence Award, 2021, 2022
The NSF EPSCoR Early Career First Award, 2022
The UNL School of Computing Teaching Excellence Award, 2022 (Graduate Level)
The IEEE Technical Committee on Cyber-Physical Systems Outstanding Ph.D. Dissertation Award, 2021

Grants

Hoang-Dung Tran (UF-PI), CPS-Medium: "Causal Reinforcement Learning for Smart Building CPS", 2025-2028.
Hoang-Dung Tran (Sole-PI), NSF CAREER: "Enabling Trustworthy Complex Learning-enabled Autonomy", 2025-2030.
Hoang-Dung Tran (Lead-PI), NSF LES Collaborative: "Foundations for Qualitative and Quantitative Safety Assessment of Learning-enabled Systems", 2023-2027.
Hoang-Dung Tran (Sole-PI), NSF FMitF Track II: "StarV: A Quantitative Verification Tool for Learning-enabled Cyber-Physical Systems", 2024-2026.
Hoang-Dung Tran(Lead-PI), Navy Phase I: "AI Monitoring & Verification (AIMV) Tool", 2023-2024.
Hoang-Dung Tran (Co-PI), Nebraska Research Initiative, "Framework for Human-Robot Interactions in Healthcare Facility Operation," 2022-2024.
Hoang-Dung Tran (PI), NSF FMitF: Track II: Enhancing the Neural Network Verification (NNV) Tool for Industrial Applications, 2022-2024.
Hoang-Dung Tran (Sole-PI), Toyota, “Verifying Complex Behaviors of Learning-enabled Autonomous Systems,” 2022-2025.
Hoang-Dung Tran (Co-PI), NSF, “REU Site: Undergraduate Research Opportunities in Unmanned Systems Foundations and Applications,” 2022-2024.
Hoang-Dung Tran (Co-PI), Ctr for Construction Research and Training “Development of Rule-Based Safety Checking System for Autonomous Heavy Construction Equipment” 2022-2023.
Hoang-Dung Tran (Sole-PI), “Event-driven Monitoring and Verification CoDesign for Distributed Learning-enabled Cyber-Physical Vehicle Systems,” Nebraska EPSCoR First Award, 2021-2022.

Teaching

Programming Language Concepts (CSCE322), UNL, Spring 2023, Fall 2023, Fall 2024, Spring 2025
Software Engineering for Robotics (CSCE460), UNL, Spring 2021, Spring 2022, Spring 2024, Spring 2025
Deep Learning and Assured Autonomy Analysis (CSCE990, CSCE492), UNL, Fall 2020, Fall 2021, Spring 2024.
Circuit Analysis, Vanderbilt University, Summer, 2018

Service

Program committee: CAV'26, L4DC'26 (Area Chair), QEST+FORMATS'25, L4DC'25, AAAI'23,24 (senior PC), HSCC'22, SAIV'24, FormaLISE'24, FoMLAS'22, 23, NSV'21,22, FE-CPS'22, 23, HSCC'21 (Repeatability Evaluation), PerCPS'23,
Program chair/organizer: SNR'21, PerCPS'23
Publicity Chair: CPS and IoT Week 2025, ICCPS 2025
Reviewer:
- NSF CPS Panel 2025, NSF CCF Panel 2024, Israel NSF 2024
- Conferences: CDC'23, ACC'17, 22, CDC'17,18, 22, 23, EMSOFT'17,18, RTSS'16,17, ICCPS'17,18, HSCC'16,17,18,19, ARCH'16,17,18,19, AAAI'21, 22
- Journals:
  - ACM Transactions on Software Engineering and Methodology (2023, 2024)
  - ACM Transactions on Cyber-Physical Systems (2024)
  - IEEE Computer (2024, 2025)
  - Elsevier Journal of Systems Architecture (2023)
  - Robotic and Automation Letters (2024)
  - IFAC Journal of Systems and Control (2024)
  - Journal of Software and Systems Modeling (2024)
  - IEEE Transactions on Systems, Man, and Cybernetics: Systems (2023, 2024)
  - IEEE Transactions on Control of Network Systems (2022, 2023)
  - IEEE Open Journal of Control Systems (2022)
  - IEEE Transactions on Automatic Control (2022)
  - IEEE Transactions on Neural Networks and Learning Systems (2022)
  - ACM Transactions on Embedded Computing Systems (2021)
  - IEEE Transactions on Software Engineering (2021, 2022)
  - IEEE Control System Letters (2021)
  - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2021, 2023)
  - Nonlinear Analysis: Hybrid Systems (2019, 2020, 2021, 2022)
  - IEEE Computer Magazine (2020)
  - Asian Journal of Control (2015)
  - IET Control Theory and Applications (2018)
  - Neuro-computing (2019, 2023)

Selected Publications

[NAHS'26] Yuntao Li, SungWoo Choi, Qing Liu, Bardh Hoxha, Georgios Fainekos, Hoang-Dung Tran: “Quantitative Verification of Learning-enabled Systems using ProbStar Reachability ”. In the Elsevier Journal of Nonlinear Analysis: Hybrid Systems, 2026 (invited paper).
[CAV'25] Hoang-Dung Tran, Sung Woo Choi, Yuntao Li, Qing Liu, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos: “StarV: A Qualitative and Quantitative Verification Tool for Learning-enabled Systems”. The 37th International Conference on Computer-Aided Verification, 2025.
[HSCC'25] Hoang-Dung Tran, Sung Woo Choi, Yuntao Li, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos: “ProbStar Temporal Logic for Verifying Complex Behaviors of Learning-enabled Systems”. In The Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control, 2025.
[ICCPS'25] Ryan Brown, Luan Viet Nguyen, Weiming Xiang, Marilyn Wolf, Hoang-Dung Tran: “Perception-based Quantitative Runtime Verification for Learning-enabled Cyber-Physical Systems”. In the Proceedings of the ACM/IEEE 16th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2025).
[NAHS'25] Sung Woo Choi, Yuntao Li, Xiaodong Yang, Tomoya Yamaguchi, Bardh Hoxha, Georgios Fainekos, Danil Prokhorov, Hoang-Dung Tran: “Reachability Analysis of Recurrent Neural Networks”. In the Elsevier Journal of Nonlinear Analysis: Hybrid Systems, 2025 (invited paper).
[MEMOCODE'24] Apala Pramanik, Sung Woo Choi, Yuntao Li, Luan Viet Nguyen, Kyungki Kim, Hoang-Dung Tran: “Perception-based Runtime Monitoring and Verification for Human-Robot Construction Systems”. In the 22nd ACM-IEEE International Symposium on Formal Methods and Models for System Design (MEMOCODE), 2024 (best paper award runner up).
[HSCC'23] Hoang Dung Tran, SungWoo Choi, Tomoya Yamaguchi, Bardh Hoxha, and Danil Prokhorov. “Verification of Recurrent Neural Networks using Star Reachability.” The 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), May 2023 .
[HSCC'23] Hoang Dung Tran, SungWoo Choi, Hideki Okamoto, Bardh Hoxha, Georgios Fainekos, and Danil Prokhorov. “Quantitative Verification of Neural Networks using ProbStars.” The 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), May 2023.
[TES'23] SungWoo Choi, Michael Ivashchenko, Luan Viet Nguyen, and Hoang-Dung Tran, "Reachability Analysis of Sigmoidal Neural Networks", IEEE Transactions on Embedded Systems, 2023.
[FormaLISE'23] Michael Ivashchenko, SungWoo Choi, Luan Viet Nguyen, and Hoang-Dung Tran, "Verification of Binary Neural Networks." The International Conference on Formal Methods in Software Engineering, 2023.
[CAV'23] Diego Manzanas Lopez, SungWoo Choi, Hoang-Dung Tran, and Taylor T. Johnson, "NNV2.0: The neural network verification tool". The 35th International Conference on Computer-Aided Verification, 2023.
[NFM'22] S. Bak and Hoang-Dung Tran, "Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability," 14th NASA Formal Methods Symposium (NFM 2022), 33% acceptance rate. [pdf]
[FORMATS'22] Xiaodong Yang, Tom Yamaguchi, Hoang-Dung Tran, Taylor T. Johnson, Bardh Hoxha, Danil Prokhorov, "Neural Network Repair with Reachability Analysis." In 20th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), vol. , no. , pp. , 2022, September. (Best Artifact Award). [pdf]
[CAV’21 ] Hoang-Dung Tran, Neelanjana Pal , Patrick Musau , Diego Manzanas Lopez , Nathaniel Hamilton , Xiaodong Yang, Stanley Bak , and Taylor T. Johnson. “Robustness Verification of Semantic Segmentation Neural Networks using Relaxed Reachability.” The 33rd International Conference on Computer-Aided Verification (CAV 2021), Los Angeles, California, USA, July 19-24, 2021, Acceptance Rate 27%. [pdf]
[TNNLS'21] Weiming Xiang, Hoang-Dung Tran, Xiaodong Yang, Taylor T. Johnson, "Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach", In IEEE Transactions on Neural Networks and Learning Systems, vol. 32, no. 5, pp. 1821-1830, 2021, May. [pdf]
[HSCC’21 ] Xiaodong Yang, Taylor T.Johnson, Hoang-Dung Tran, Tomoya Yamaguchi, Bardh Hoxha, and Danil Prokhorov. “Reachability Analysis of Deep ReLU Networks using Facet-Vertex Incidence.” The 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), April 2021 . [pdf]
[CAV’20 ] Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak and Taylor T.Johnson. “NNV: A Tool for Verification of Deep Neural Networks and Learning-Enabled Cyber-Physical Systems.” The 32nd International Conference on Computer-Aided Verification (CAV 2020), Los Angeles, California, USA, July 19-24, 2020, Acceptance Rate 27% .[pdf]
[CAV’20 ] Hoang-Dung Tran, Stanley Bak, Weiming Xiang, and Taylor T.Johnson. “Verification of Deep Convolutional Neural Networks using ImageStars..” The 32nd International Conference on Computer-Aided Verification (CAV 2020), Los Angeles, California, USA, July 19-24, 2020, Acceptance Rate 27% .[pdf]
[CAV’20 ] Stanley Bak, Hoang-Dung Tran, and Taylor T.Johnson. “Improved Geometric Path Enumeration for Verifying ReLU Neural Networks.” The 32nd International Conference on Computer-Aided Verification (CAV 2020), Los Angeles, California, USA, July 19-24, 2020, Acceptance Rate 27%.[pdf]
[IEEE-D&T’20 ] Hoang-Dung Tran, Weiming Xiang, Taylor T. Johnson. “Verification Approaches for Autonomous Learning-enabled Cyber-Physical Systems.” IEEE Design & Test, 2020.[pdf]
[FM’19 ] Hoang-Dung Tran, Diego Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, and Taylor T.Johnson. “Star-Based Reachability Analysis for Deep Neural Networks.” The 23rd International Symposium on Formal Methods, Porto, Portugal, 2019, Acceptance Rate 30%.[pdf]
[EMSOFT’19 ] Hoang-Dung Tran, Feiyang Cei, Diego Manzanas Lopez, Taylor T.Johnson, and Xenofon Koutsoukos. “Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control.” The International Conference on Embedded Software, New York, October, 2019. Acceptance Rate 26%.[pdf]
[FORTE’19 ] Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau, Weiming Xiang, and Taylor T. Johnson. “Decentralized Real-Time Safety Verification for Distributed Cyber-Physical Systems.” The 39th International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Copenhagen, Denmark, Jun 17-21, 2019, Acceptance Rate 42.8%.[pdf]
[FORMATS’19 ] Hoang-Dung Tran, Luan Viet Nguyen, Nathaniel Hamilton, Weiming Xiang, and Taylor T.Johnson. “Reachability Analysis for High-Index Linear Differential Algebraic Equations.” The 17th International Conference on Formal Modeling and Analysis of Timed Systems, Amsterdam, The Netherlands, August 26-31, 2019, Acceptance Rate 40%.[pdf]
[HSCC’19 ] Stanley Bak, Hoang-Dung Tran, and Taylor T.Johnson. “Numerical verification of affine systems with up to a billion dimensions.” The 22nd ACM International Conference on Hybrid Systems: Computation and Control, Montreal, Canada, April 2019, Acceptance rate: 25%.[pdf]
[IEEE-TAC’19 ] Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson. “Nonconservative Lifted Convex Conditions for Stability of Discrete-Time Switched Systems Under Minimum Dwell-Time Constraint.” IEEE Transactions on Automatic Control, 64(8), 3407-3414 , 2019.[pdf]
[ADHS’18 ] Hoang-Dung Tran, Weiming Xiang, Stanley Bak and Taylor T. Johnson. “Reachability Analysis for One Dimensional Linear Parabolic Equations.” The IFAC Conference on Analysis and Design of Hybrid Systems, Oxford, UK, July 2018.[pdf]
[IEEE-TNNLS’18 ] Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson. “Output reachable set estimation and verification for multi-layer neural networks.” IEEE Transactions on Neural Networks and Learning Systems, 29(11), 5777 - 5783, 2018.[pdf]
[DEDS’17 ] Hoang-Dung Tran, Luan Nguyen, Weiming Xiang, Taylor T. Johnson. “Order-reduction abstractions for safety verification of high-dimensional linear systems.” Discrete Event Dynamic Systems, 27(2), 443–461, 2017.[pdf]
[IEEE-TAC’17 ] Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson. “Robust exponential stability and disturbance attenuation for discrete-time switched systems under arbitrary switching.” IEEE Transactions on Automatic Control, 63(5), 1450-1456, 2017.[pdf]
[IEEE-TEC’14 ] Luan Viet Nguyen, Hoang-Dung Tran, Taylor T. Johnson. “Virtual Prototyping for Distributed Control of a Fault-Tolerant Modular Multilevel Inverter for Photovoltaics.” IEEE Transactions on Energy Conversion, vol. 29, pp. 841-850, December 2014.[pdf]
[ISA’13 ] Hoang-Dung Tran, Zhi-Hong Guan, Xuan-Kien Dang, Xin-Ming Cheng, Fu-Shun Yuan. “A normalized PID controller in networked control systems with varying time delays.” ISA Transaction, September, 2013.[pdf]

Page updated

Google Sites

Report abuse