Mingshuai Chen

Click to reveal
Room 4230
Ahornstraße 55
D-52074 Aachen
+49 241 80 21208

I am a postdoctoral researcher at the Software Modeling and Verification Group (MOVES) headed by Prof. Joost-Pieter Katoen associated with the ERC Advanced Grant Project FRAPPANT: Formal Analysis of Probabilistic Programs. In 2019, I received the Ph.D. degree (with my dissertation titled Verification and Synthesis of Time-Delayed Dynamical Systems) in computer science from the Institute of Software, Chinese Academy of Sciences, under the supervision of Prof. Naijun Zhan and co-supervision of Prof. Martin Fränzle. For detailed information, please check my CV.


My research interests include

  • formal verification of probabilistic programs
  • modelling, verification and synthesis of hybrid systems
  • reachability analysis
  • interpolant/invariant synthesis
  • time-delayed systems
  • cyber-physical systems

See the bottom of this page for a list of publications. For the list of tools and case studies that I was involved in during my doctoral research, please check my homepage at ISCAS.

You can also find me on
View Mingshuai Chen's profile on LinkedIn

Thesis Topics

If you are interested in writing a Bachelor/Master’s thesis in any of the aforementioned topics, don’t hesitate to contact me. You can also check our list of open topics.

Topics Open

Academic Services

Teaching Assistant

Committee Member

External Reviewer


Conferences & Workshops

Honors & Awards

Selected Talks

Ph.D. Defence


Conferences, Seminars & Visits

Publications (till 2019)

Book Chapters


Peer-Reviewed Conferences

Publications (since 2020)

DOI fulltext PDF [bibtex]
title = {Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control},
author = {Mingshuai Chen and Martin Fränzle and Yangjia Li and Peter N. Mosaad and Naijun Zhan},
publisher = {Springer},
journal = {Acta informatica},
pages = {32 Seiten},
type = {Journal Article},
year = {2020},
doi = {10.1007/s00236-020-00374-7},
url = { https://publications.rwth-aachen.de/record/783310},
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, Naijun Zhan. Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control, Acta informatica, 32 Seiten, Springer, 2020.
DOI fulltext PDF [bibtex]
title = {Learning One-Clock Timed Automata},
author = {Jie An and Mingshuai Chen and Bohua Zhan and Naijun Zhan and Miaomiao Zhang},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078},
pages = {444-462},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_25},
url = { https://publications.rwth-aachen.de/record/787949},
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning One-Clock Timed Automata, The 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078 of LNCS, 444-462, Springer, 2020.
DOI fulltext PDF [bibtex]
title = {Unbounded-Time Safety Verification of Stochastic Differential Dynamics},
author = {Shenghua Feng and Mingshuai Chen and Bai Xue and Sriram Sankaranarayanan and Naijun Zhan},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {327-348},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_18},
url = { https://publications.rwth-aachen.de/record/794357},
Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan. Unbounded-Time Safety Verification of Stochastic Differential Dynamics, 32nd International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 327-348, Springer, 2020.
Show all