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


  • Formal Analysis, Verification and Design of Safety-Critical CPS. RTSS, Hong Kong, China, Dec. 2019. RTSS-HTD Tutorial co-presented with Lei Bu, Qixin Wang and Naijun Zhan.

Conferences, Seminars & Visits

Publications (till 2019)

Book Chapters


Peer-Reviewed Conferences

Publications (since 2020)

DOI fulltext PDF [bibtex] Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan. Unbounded-Time Safety Verification of Stochastic Differential Dynamics, The 32nd International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, pages 327-348, Springer, 2020.
DOI fulltext PDF [bibtex] 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, pages 444-462, Springer, 2020.
DOI fulltext PDF [bibtex] 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 , 2020.