Rong Gu, Post Doc

Personal homepage:

Education Background:

  • Ph.D. of Computer Science, Mälardalen University, Sweden, 2017 - 2022.
  • Master of Engineer in Software Engineering School, Xi'an Jiaotong University, China, 2010-2013.
  • Bachelor in Software Engineering School, Xi'an Jiaotong University, China, 2006-2010.
Rong had been working as an embedded system engineer in a top avionic institute in China from 2013 - 2017. His work covers the embedded software development of the safety-critical systems deployed in aircrafts, trains, etc, as well as tools for system simulation, testing, and demonstration. He has a rich experience of model-based software engineering and the relevant methods and tools, e.g., SysML, AADL, Simulink, etc.


Rong's research is problem oriented and closely connected to real-world problems. He has worked with many industrial partners, e.g., Volvo Construction Equipment, and Volvo cars. His goal of the research is to synthesize correctness-guaranteed controllers for autonomous systems and the testers to find potential design errors in the early time of development by using his tools that are based on formal methods. His research interest is listed but not limited as follows:

  • Formal modelling and verification of embedded systems (discrete models, hybrid models, etc.)
  • Formal specification of requirements
  • Machine Learning, Reinforcement Learning
  • Controller synthesis of linear and nonlinear dynamic systems
  • Tools I use: UPPAAL (SMC)UPPAAL Stratego. Tools I develop: MALTA, to be continued...



Rong is actively involved in supervising postgraduate students' thesis and teaching the following courses:

  • DAV231: Development of Web Application (2017 - 2019)
  • DVA218: Data Communication (2018 - now)
  • DVA468: Catching Bugs by Formal Verification (2018 - now)
  • DVA128: Program with Python (2022 - 2023)
  • Embedded System II: a guest lecture (2021)


He has supervised the following Master/Bachelor theses:

  • Overcoming the ambiguity and inconsistency of requirements by using generative AI. 2024.
  • Model Checked Reinforcement Learning For Multi-Agent Planning. 2023.
  • Safety-Guaranteed Mission Planner for Autonomous Vehicles (2020)

Research topic:

Autonomous systems, such as self-driving cars, drones, and autonomous construction equipment, are safety-critical and thus are supposed to operate autonomously with very high dependability. My research mainly focuses on applying formal verification in the development of autonomous systems. Formal verification benefits finding design errors that are difficult to be discovered in the early phases of development or reappeared in the laboratory. With the help of formal verification, we can not only find bugs but also prove the absence of bugs in autonomous systems.

I am also working on providing advanced methods and tools to synthesize controllers of autonomous systems operating in a closed environment. Those controllers are generated automatically and are guaranteed to be correct in the sense that they must satisfy the requirements of the systems, e.g., never collide with any obstacles in the environment.


  • MALTA has been published on GitHub (click here). The tool is for solving the pathfinding and task scheduling problems of multi-agent systems. The introduction video of the tool: click here. Co-authors of the tool: Afshin AmeriBaran Çürüklü, and Eduard Baranov (from UCLouvain). 
  • MCRL (Model Checking + Reinforcement Learning) for mission planning of multi-agent systems is being integrated into UPPAAL Stratego through a collaboration with Aalborg University.


Recent experience:

  • February 2024 - I attend Dagstuhl Seminar 24071 - Safety Assurance for Autonomous Mobility.
  • October 2023 - tool-demo chair of ECBS 2023
  • October 2023 - I give a presentation at AISoLA 2023.
  • September 2023 - I give a presentation at QUATIC 2023 (16th International Conference on the Quality of Information and Communications Technology).
  • April 2023 - I give a presentation at A-MOST 2023 (19th Workshop on Advances in Model Based Testing).
  • June 2022 - I have defended my doctoral dissertation "Formal Methods for Scalable Synthesis and Verification of Autonomous Systems". The opponent of the defense was Professor Rajeev Alur, from the University of Pennsylvania.
  • November 2021 - I have given a presentation in FM'21 (24th International Symposium of Formal Methods). The video of the presentation is online (click here).
  • October 2021 - I have given a presentation in ISoLA2021 (10th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation). The video of the presentation is online (click here).
  • May 2021 - I have given a presentation of my research for the MER 21 evaluation of MDH (click here).
  • September 2020 - I have participated in the 25th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2020) and given a presentation about our paper: Verifiable and Scalable Mission-Plan Synthesis for Multiple Autonomous Agents. This paper has honourably won the Best-paper Award. The presentation is available online (click here).
  • June 2020 - I have attended the 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP) and given a presentation about my research: Controller Synthesis and Verification for Multi-Agent Systems.
  • June 2020 - I have defended my licentiate thesis: Automatic Model Generation and Scalable Verification for Autonomous Vehicles - Mission Planning and Collision Avoidance. The opponent of the defense was Professor Kim Larsen, from Aalborg University.
  • April 2020 - I have participated in the 35th ACM/SIGAPP Symposium On Applied Computing (SAC 2020) and given a presentation about our paper: TAMAA: UPPAAL-based Mission Planning for Autonomous Agents. The presentation is available online (click here).
  • November 7, 2019 - I have given a presentation about our research and tool (TAMAA) in the VCE/MDH Partnership Celebration, Eskilstuna, Sweden.
  • June 10, 2019 - I have attended the 2019 Summer School on Cyber-Physical Systems in KTH, Stockholm, Sweden.
  • May 9, 2019 - I have given a presentation at the 11th Annual NASA Formal Methods Symposium (NFM 2019) in Houston, USA - Towards a Two-layer Framework for Verifying Autonomous Vehicles.
  • April 22, 2019 - I have attended the 12th IEEE Conference on Software Testing, Validation and Verification (ICST 2019) in Xi'an, China.
  • Feb 14, 2019 - I have given a presentation at the workshop: Formal Verification - Secure SW Functions for Operating Autonomous Machine with Humans in VOLVO Construction Equipment.
  • Aug 13, 2018 - I have attended the Marktoberdorf Summer School 2018.
  • Jun 2, 2018 - I have given a presentation at the 6th FormaliSE 2018 (International Conference on Formal Methods in Software Engineering) about our paper: Formal Verification of an Autonomous Wheel Loader using Model Checking.
  • Apr 25, 2018 - I have given a presentation about the formal verification of autonomous vehicles at DPAC summit 2018.
  • Apr 9 - 13, 2018 - I have participated in the 11th ICST as a volunteer. 

[Show all publications]

[Google Scholar author page]

Latest publications:

Guess and then Check: Controller Synthesis for Safe and Secure Cyber-Physical Systems (Jul 2024)
Rong Gu, Zahra Moezkarimi, Marjan Sirjani
44th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2024)

Synthesis and Verification of Mission Plans for Multiple Autonomous Agents under Complex Road Conditions (Jun 2024)
Rong Gu, Eduard Baranov , Afshin Ameri E., Eduard Paul Enoiu, Baran Çürüklü, Cristina Seceleanu, Axel Legay , Kristina Lundqvist
ACM Transactions on Software Engineering and Methodology (TOSEM)

Pattern-Based Verification of ROS 2 Nodes using UPPAAL (Sep 2023)
Lukas Dust, Rong Gu, Cristina Seceleanu, Mikael Ekström, Saad Mubeen
FMICS 2023 - International Conference on Formal Methods for Industrial Critical Systems (FMICS 2023)

Experimental Evaluation of Callback Behavior in ROS 2 Executors (Sep 2023)
Lukas Dust, Emil Persson, Mikael Ekström, Saad Mubeen, Cristina Seceleanu, Rong Gu
28th International Conference on Emerging Technologies and Factory Automation (ETFA 2023)

Model-Based Policy Synthesis and Test-Case Generation for Autonomous Systems (Apr 2023)
Rong Gu, Eduard Paul Enoiu
19th Workshop on Advances in Model Based Testing (A-MOST 2023)

Correctness-Guaranteed Strategy Synthesis and Compression for Multi-Agent Autonomous Systems (Sep 2022)
Rong Gu, Peter Jensen , Cristina Seceleanu, Eduard Paul Enoiu, Kristina Lundqvist
Science of Computer Programming (SCICO-223)