Verification and Validation for Assured Autonomy

Hoang-Dung Tran

University of Nebraska-Lincoln

School of Computing

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

Bio: I am an Assistant Professor in the School of Computing at the University of Nebraska, Lincoln. 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. I am a co-director of the NIMBUS Lab at UNL where I lead the Verification and Validation for Assured Autonomy Group.

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: Event-Driven Monitoring and Verification for Distributed Learning-enabled Cyber-Physical Systems
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

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(Lead-PI), Navy Phase I: "AI Monitoring & Verification (AIMV) Tool", 2023-2024.
Hoang-Dung Tran (Lead-PI), NSF LES Collaborative: "Foundations for Qualitative and Quantitative Safety Assessment of Learning-enabled Systems", 2023-2026.
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-2024.
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
Software Engineering for Robotics (CSCE460), UNL, Spring 2021, Spring 2022, Spring 2024.
Deep Learning and Assured Autonomy Analysis (CSCE990, CSCE492), UNL, Fall 2020, Fall 2021, Spring 2024.
Circuit Analysis, Vanderbilt University, Summer, 2018

Service

Program committee: AAAI'23,24 (senior PC), HSCC'22, SAIV'24, FoMLAS'22, 23, NSV'21,22, FE-CPS'22, 23, HSCC'21 (Repeatability Evaluation), PerCPS'23
Program chair/organizer: SNR'21, PerCPS'23
Reviewer:
- Conferences: 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)
  - Elsevier Journal of Systems Architecture (2023)
  - 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)

Selected Publications

[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]