Formal verification of an autonomous wheel loader by model checking. - Rong Gu 002; Raluca Marinescu; Cristina Seceleanu; Kristina Lundqvist (FormaliSE@ICSE, 2018)

Towards a Two-Layer Framework for Verifying Autonomous Vehicles. - Rong Gu 002; Raluca Marinescu; Cristina Seceleanu; Kristina Lundqvist (NFM, 2019)

Verifiable and Scalable Mission-Plan Synthesis for Autonomous Agents. - Rong Gu 002; Eduard Enoiu; Cristina Seceleanu; Kristina Lundqvist (FMICS, 2020)

Probabilistic Mission Planning and Analysis for Multi-agent Systems. - Rong Gu 002; Eduard Enoiu; Cristina Seceleanu; Kristina Lundqvist (ISoLA (1), 2020)

TAMAA: UPPAAL-based mission planning for autonomous agents. - Rong Gu 002; Eduard Enoiu; Cristina Seceleanu (SAC, 2020)

Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. - Rong Gu 002; Cristina Seceleanu; Eduard Enoiu; Kristina Lundqvist (FM, 2021)

Correctness-guaranteed strategy synthesis and compression for multi-agent autonomous systems. - Rong Gu 002; Peter Gjøl Jensen; Cristina Seceleanu; Eduard Enoiu; Kristina Lundqvist (Sci. Comput. Program., 2022)

Verifiable strategy synthesis for multiple autonomous agents: a scalable approach. - Rong Gu 002; Peter Gjøl Jensen; Danny Bøgsted Poulsen; Cristina Seceleanu; Eduard Enoiu; Kristina Lundqvist (Int. J. Softw. Tools Technol. Transf., 2022)

Formal Methods for Scalable Synthesis and Verification of Autonomous Systems : Mission Planning and Collision Avoidance. - Rong Gu 002 (2022)

Learning in Uppaal for Test Case Generation for Cyber-Physical Systems. - Rong Gu 002 (ECBS, 2023)

Experimental Evaluation of Callback Behavior in ROS 2 Executors. - Lukas Johannes Dust; Emil Persson; Mikael Ekström; Saad Mubeen; Cristina Seceleanu; Rong Gu 002 (ETFA, 2023)

Pattern-Based Verification of ROS 2 Nodes Using UPPAAL. - Lukas Johannes Dust; Rong Gu 002; Cristina Seceleanu; Mikael Ekström; Saad Mubeen (FMICS, 2023)

Model-Based Policy Synthesis and Test-Case Generation for Autonomous Systems. - Rong Gu 002; Eduard Enoiu (ICSTW, 2023)

A Service-Oriented Digital Twin Framework for Dynamic and Robust Distributed Systems. - Rong Gu 002; Tiberiu Seceleanu; Ning Xiong 001; Muhammad Naeem 012 (SSE, 2024)

Experiences in Building a Digital Twin Framework: Challenges and Possible Solutions. - Rong Gu 002; Teodor Barbuceanu; Ning Xiong 001; Tiberiu Seceleanu (COMPSAC, 2024)

UPPAAL-Based Modeling and Verification of ROS 2 Multi-threaded Execution and Operating System Reservations. - Lukas Johannes Dust; Rong Gu 002; Cristina Seceleanu; Mikael Ekström; Saad Mubeen (FMICS, 2024)

Guess and Then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems. - Rong Gu 002; Zahra Moezkarimi; Marjan Sirjani (FORTE, 2024)

CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles. - Rong Gu 002; Kaige Tan; Andreas Holck Høeg-Petersen; Lei Feng 002; Kim Guldstrand Larsen (ISoLA (3), 2024)

A Model-Based Methodology for Automated Verification of ROS 2 Systems. - Lukas Johannes Dust; Mikael Ekström; Rong Gu 002; Saad Mubeen; Cristina Seceleanu (RoSE, 2024)

Energy-Efficient Motion Planning for Autonomous Vehicles Using Uppaal Stratego. - Muhammad Naeem 011; Rong Gu 002; Cristina Seceleanu; Kim Guldstrand Larsen; Brian Nielsen; Michele Albano (TASE, 2024)

Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions. - Rong Gu 002; Eduard Baranov; Afshin Ameri; Cristina Seceleanu; Eduard Paul Enoiu; Baran Çürüklü; Axel Legay; Kristina Lundqvist (ACM Trans. Softw. Eng. Methodol., 2024)

Modelling Cyber-Physical Systems for Verification and Synthesis. - Rong Gu 002 (Rebeca for Actor Analysis in Action, 2025)

Formal Methods in Industry. - Maurice H. ter Beek; Rod Chapman; Rance Cleaveland; Hubert Garavel; Rong Gu 002; Ivo ter Horst; Jeroen J. A. Keiren; Thierry Lecomte; Michael Leuschel; Kristin Yvonne Rozier; Augusto Sampaio 001; Cristina Seceleanu; et al. (Formal Aspects Comput., 2025)

A model-based approach to automation of formal verification of ROS 2-based systems. - Lukas Johannes Dust; Rong Gu 002; Saad Mubeen; Mikael Ekström; Cristina Seceleanu (Frontiers Robotics AI, 2025)

Pattern-based verification of ROS 2 applications using UPPAAL. - Lukas Johannes Dust; Rong Gu 002; Cristina Seceleanu; Mikael Ekström; Saad Mubeen (Int. J. Softw. Tools Technol. Transf., 2025)