Cristina Seceleanu, Associate Professor

Cristina Seceleanu is Associate Professor and Docent at MDH, Networked and Embedded Systems (NES) Division. She received a MSc. in Electronics from Polytechnic University of Bucharest, Romania, in 1993, and a Ph.D. in Computer Science from Åbo Akademi and Turku Centre for Computer Science, Åbo/Turku, Finland, in Dec. 2005. Her research focuses on developing formal models and verification techniques for designing predictable real-time embedded systems.


  • DVA 241 - Distributed Systems (undergraduate course): 2018, 2017
  • DVA 468 - Catching Bugs by Formal Verification (PROMPT course): 2018, 2017
  • CDT 316 - Distributed Systems (undergraduate course): 2016, 2015, 2014, 2013
  • DVA 442 - Advanced Validation and Verification (graduate, distance course) : 2017, 2016, 2015
  • DVA 402 - Advanced Validation and Verification (graduate course): 2012, 2011, 2010
  • CDT 505 - Real-Time Systems II (graduate course): 2012, 2011, 2009, 2008
  • The Science of Programming (Ph.D. course): 2009




Cristina Seceleanu's research focuses on developing and applying formal methods (especially model checking) for designing and reasoning about component-based, resource-constrained real-time systems, service-oriented systems, adaptive embedded systems, and more recently autonomous systems. The goal is to provide mathematical means of predicting system behaviors at early stages of development.

Cristina is leading the Formal Modeling and Analysis of Embedded Systems research group, at MDH, and has been teacher representative for Embedded Systems, IDT, in the committee for research of the faculty board (Utskottet för forskning), 2015-2016. 

Cristina is co-author of the following integrated development environments (IDE) / toolchains that implement the research results obtained together with wonderful collaborators:

  • REMES IDE    : developed as a cooperation between projects DICES and PROGRESS. It supports the construction and analysis of embedded system behavioral models described in the REMES language. REMES is a hierarchical, dense-time language for modeling function, time and resource usage of embedded components. The REMES IDE consists of a set of tools, as follows: (i) REMES editor, (ii) automated transformations of REMES models into priced timed automata for formal analysis and verification, and (iii) REMES simulator of the timing behavior and resource consumption of embedded components, at design time. Together with Aneta Vulgarakis Feljan, Ericsson Research, Stockholm, and Marin Orliς, Ericsson Nikola Tesla, Zagreb.


  • ViTAL toolchain      a verification tool tailored for the architectural language EAST-ADL, in which functional and timing behaviors of function prototypes are expressed as timed automata models that have precise semantics and can be formally verified. The ViTAL tool enables the automatic transformation of EAST-ADL functional models into UPPAAL PORT or UPPAAL, for model checking. Together with Raluca Marinescu, Eduard Paul Enoiu, and Paul Pettersson.


Editorial Boards:


PC Chair and Organizer of:


Program Committees (selection): 

  • 37th Annual IEEE Computer Software and Applications Conference (COMPSAC 2013), Workshops Chair, July 22-26, 2013 - Kyoto, Japan.
  • 6th IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE 2012), July 4-6, 2012 - Beijing, China.



[Show all publications]

[Google Scholar author page]

Latest publications:

Probabilistic Mission Planning and Analysis for Multi-agent Systems (Oct 2020)
Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu, Kristina Lundqvist
9th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020)

Verifiable and Scalable Mission-Plan Synthesis for Multiple Autonomous Agents (Sep 2020)
Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu, Kristina Lundqvist

Specification and Automated Verification of Atomic Concurrent Real-time Transactions (Jul 2020)
Simin Cai, Barbara Gallina, Dag Nyström, Cristina Seceleanu
Software and Systems Modeling (SoSym)

Combining Model Checking and Reinforcement Learning for Scalable Mission Planning of Autonomous Agents (May 2020)
Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu, Kristina Lundqvist

DPAC Newsletter Spring 2020 (May 2020)
Kristina Lundqvist, Mikael Sjödin, Saad Mubeen, Håkan Forsberg, Mikael Ekström, Cristina Seceleanu, Nandinbaatar Tsog, Jakob Danielsson, Mohammad Loni, Baran Çürüklü, LanAnh Trinh, Afshin Ameri E., Luciana Provenzano, Kaj Hänninen, Susanne Fronnå, Marjan Sirjani, Rong Gu, Masoud Daneshtalab, Sima Sinaei, Joakim Lindén

TAMAA: UPPAAL-based Mission Planning for Autonomous Agents (Apr 2020)
Rong Gu, Eduard Paul Enoiu, Cristina Seceleanu
The 35th ACM/SIGAPP Symposium On Applied Computing (SAC2020)

PhD students supervised as main supervisor:

Ashalatha Kunnappilly
Nesredin Mahmud
Predrag Filipovikj (former)
Raluca Marinescu (former)
Rong Gu
Simin Cai

PhD students supervised as assistant supervisor:

Aida Causevic (former)
Aneta Vulgarakis Feljan (former)
Jagadish Suryadevara (former)
Leo Hatvani (former)
Stefan Björnander (former)