Mingshuai Chen

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

I have become an Assistant Professor leading the Formal Verification Group at Zhejiang University. Check my current homepage here.

Prior to joining ZJU, I worked as a postdoctoral researcher at the Software Modeling and Verification Group 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.


I develop formal reasoning techniques for programs and hybrid systems for ensuring the reliability and effectiveness of safety-critical software systems while pushing the limits of automation as far as possible. My primary research interests include

  • semantics, verification, and synthesis of probabilistic programs
  • modelling, verification, and synthesis of hybrid systems
  • reachability/stability/termination analysis
  • invariant/interpolant/controller synthesis
  • stochastic/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
ORCID logo View Mingshuai Chen's profile on LinkedIn

Thesis/Intern Topics

If you are interested in doing an internship or 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 Ongoing

  • Latticed Craig Interpolation with an Application to Probabilistic Programs (Intern, Zhiang Wu (HKUST))

Topics Closed

Academic Services

Teaching Assistant

Committee Member

External Reviewer


Conferences & Workshops

Honors & Awards

Selected Talks

Dissertation Defence


Conferences, Workshops, Seminars & Visits

Publications (till 2019)

Book Chapters

Peer-Reviewed Journal Articles

Peer-Reviewed Conference Papers

Publications (since 2020)

fulltext PDF [bibtex]
title = {Exact Probabilistic Inference Using Generating Functions},
author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen},
type = {Preprint},
year = {2023},
url = { https://publications.rwth-aachen.de/record/862300},
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023.
DOI fulltext PDF [bibtex]
title = {Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions},
author = {Mingshuai Chen and Joost-Pieter Katoen and Lutz Klinkenberg and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {13371},
pages = {79-101},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-13185-1_5},
url = { https://publications.rwth-aachen.de/record/848175},
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions, 34. International Conference on Computer Aided Verification (CAV 2022), Volume 13371 of LNCS, 79-101, Springer, 2022.
DOI [bibtex]
title = {Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Information and computation},
volume = {289(A)},
pages = {pages 104965},
type = {Journal Article},
year = {2022},
doi = {10.1016/j.ic.2022.104965},
url = { https://publications.rwth-aachen.de/record/853946},
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen. Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming, Information and computation 289 (A), pages 104965, Elsevier, 2022.
Show all