Selected Publications

Frontiers in Robotics and AI, 2025: A model-based approach to automation of formal verification of ROS 2-based systems. L Dust, R Gu, C Seceleanu, M Ekström, S Mubeen. [Link]

MarjanFest, 2025: Modelling Cyber-Physical Systems for Verification and Synthesis. R Gu. [Link]

FMAS'24: Model Checking for Reinforcement Learning in Autonomous Driving: One Can Do More Than You Think! R Gu. [Link].

Formal Aspects of Computing, 2024. Formal methods in industry. ter Beek MH, Chapman R, Cleaveland R, Garavel H, Gu R, ter Horst I, Keiren JJ, Lecomte T, Leuschel M, Rozier KY, Sampaio A, Seceleanu C, Martyn T, Willemse T, Zhang LJ. [Link]

ACM Transactions on Software Engineering and Methodology, 2024. Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions. R Gu, E Baranov, A Ameri, C Seceleanu, E Enoiu, B Crukulu, A Legay, K Lundqvist. [BibTex][PDF].

Report of Dagstuhl Seminar 24071, 2024. Safety Assurance for Autonomous Mobility. [Link]

ISoLA'24: CommonUppRoad: A Framework of Formal Modelling, Verifying, Learning, and Visualisation of Autonomous Vehicles. R Gu, T Kaige, A  Høeg-Petersen, L Feng, K Larsen. [website][Link]

FMICS'24: UPPAAL-based Modeling and Verification of ROS 2 Multi-Threaded Execution and Operating System Reservations. L Dust, R Gu, C Seceleanu, M Ekström, S Mubeen. [Link]

TASE'24: Energy-Optimized Motion Planning for Autonomous Vehicles Using UPPAAL Stratego. Muhammad Naeem, Rong Gu, Cristina Seceleanu, Kim Guldstrand Larsen, Brian Nielsen and Michele Albano. [Link]

FORTE'24: Guess and then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems. R Gu, Z Moezkarimi, M Sirjani. [BibTex][website]

LiVe'24: Integrating the Power of Machine Learning and Model Checking in Safety-Critical Systems. R Gu. [BibTex][PDF]

FM'24: Journal-first paper: Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems.

AISoLA'23: Studying Formal Models Using ChatGPT. P Backeman, R Gu, F Lorber. [BibTex][PDF]

FMICS'23: Pattern-Based Verification of ROS 2 Nodes Using UPPAAL. L Dust, R Gu, C Seceleanu, M Ekström, S Mubeen. [website]

ETFA'23: Experimental Evaluation of Callback Behavior in ROS 2 Executors. Lukas Dust, Emil Persson, Mikael Ekström, Saad Mubeen, Cristina Seceleanu, Rong Gu. [website]

QUATIC'23: Journal-first paper: Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems.

A-MOST'23: Model-Based Policy Synthesis and Test-Case Generation for Autonomous Systems. R Gu, E Enoiu. [BibTex][PDF][website].

Science of Computer Programming, 2022, vol. 224: Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems. R Gu, P Jensen, C Seceleanu, E Enoiu, K Lundqvist. [BibTex][PDF].

Doctoral Dissertation: Formal Methods for Scalable Synthesis and Verification of Autonomous Systems - Mission Planning and Collision Avoidance. R Gu. [BixTex][PDF] 

Software Tools for Technology Transfer, 2022, vol.24: Verifiable Strategy Synthesis for Multiple Autonomous Agents: A Scalable Approach. R Gu, P Jensen, D Poulsen, C Seceleanu, E Enoiu, K Lundqvist. [BibTex][PDF].

FM'21: Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. R Gu, C Seceleanu, E Enoiu, K Lundqvist. [BibTex] [PDF].

ISoLA'21: Probabilistic Mission Planning and Analysis for Multi-Agent Systems. R Gu, E Enoiu, C Seceleanu, K Lundqvist. [BibTex] [PDF].

FMICS'20: Verifiable and Scalable Mission-Plan Synthesis for Autonomous Agents. R Gu, E Enoiu, C Seceleanu, K Lundqvist. Best-paper Award.  [BibTex] [PDF].

SAC'20: TAMAA: UPPAAL-based Mission Planning for Autonomous Agents. R Gu, E Enoiu, C Seceleanu. [BibTex] [PDF].

NFM'19: Towards a Two-Layer Framework for Verifying Autonomous Vehicles. R Gu, R Marinescu, C Seceleanu, K Lundqvist. [BibTex] [PDF].

FormaliSE'18: Formal Verification of an Autonomous Wheel Loader by Model Checking. R Gu, R Marinescu, C Seceleanu, K Lundqvist. [BibTex] [PDF].