Mingshuai Chen


chenms at cs.rwth-aachen.de
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.

new Tutorial @ RTSS 2019: Formal analysis, verification and design of safety-critical CPS.


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

Bachelor/Master Thesis Topics


Academic Services

Teaching Assistant

  • Theories of Programming (UCAS, WS 19/18)

Organizer & Volunteer

External Reviewer


Conferences & Workshops

Honors & Awards

Selected Talks (till 2019)


  • 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.

Ph.D. Defence

Conferences, Seminars & Visits

Publications (till 2019)

Book Chapters

  1. Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, and Liang Zou. MARS: A toolchain for modelling, analysis and verification of hybrid systems. In Provably Correct Systems (ProCoS 2015), NASA Monographs in Systems and Software Engineering, pp. 39-58. Springer International Publishing, 2017.


  1. Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan. Indecision and delays are the parents of failure – Taming them algorithmically by synthesizing delay-resilient controlActa Informatica. Under minor revision.
  2. Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, and Ting Gan. From model to implementation: A network-algorithm programming languageSCIENCE CHINA Information Sciences. Under minor revision.
  3. Martin Fränzle, Mingshuai Chen, and Paul Kröger. In memory of Oded Maler: Automatic reachability analysis of hybrid-state automata. In ACM SIGLOG News, vol. 6, no. 1, pp. 19-39.
  4. Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan. Reachability analysis for solvable dynamical systems. In IEEE Trans. Automat. Contr., vol. 63, no. 7, pp. 2003-2018.

Peer-Reviewed Conferences

  1. Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan. NIL: Learning nonlinear interpolants. In Proc. of CADE 2019, LNCS 11716, pp. 178-196. Extended version [typos in Theorem 1 & Table 2 corrected].
  2. Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue. Taming delays in dynamical systems – Unbounded verification of delay differential equations. In Proc. of CAV 2019, LNCS 11561, pp. 650-669. (Arfifact Evaluated).
  3. Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan. What’s to come is still unsure – Synthesizing controllers resilient to delayed interaction. In Proc. of ATVA 2018, LNCS 11138, pp. 56-74. (Distinguished Paper Award)Extended version.
  4. Bai Xue, Peter N. Mosaad, Martin Fränzle, Mingshuai Chen, Yangjia Li, and Naijun Zhan. Safe over- and under-approximation of reachable sets for delay differential equations. In Proc. of FORMATS 2017, LNCS 10419, pp. 281-299.
  5. Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan. Validated simulation-based verification of delayed differential dynamics. In Proc. of FM 2016, LNCS 9995, pp. 137-154. Extended version.
  6. Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, and Mingshuai Chen. Interpolant synthesis for quadratic polynomial inequalities and combination with EUF [typos in Table 1 corrected]. In Proc. of IJCAR 2016, LNCS 9706, pp. 195-212.
  7. Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, and Naijun Zhan. A two-way path between formal and informal design of embedded systems. In Proc. of UTP 2016, LNCS 10134, pp. 65-92. Extended version.
  8. Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan. Computing reachable sets of linear vector fields revisited. In Proc. of ECC 2016, IEEE-Xplore, pp. 419-426.
  9. Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, and Naijun Zhan. Decidability of the reachability for a family of linear vector fields. In Proc. of ATVA 2015, LNCS 9364, pp. 482-499.