Mingshuai Chen

cms
Email
Click to reveal
Address
Room 4230
Ahornstraße 55
D-52074 Aachen
Phone
+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.

Research

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

Journals

Conferences & Workshops

Honors & Awards

Selected Talks

Dissertation Defence

Tutorials

Conferences, Workshops, Seminars & Visits

Publications (till 2019)

Book Chapters

Peer-Reviewed Journal Articles

Peer-Reviewed Conference Papers

Publications (since 2020)

2023
fulltext PDF [bibtex]
@unpublished{EPIUGF2023,
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},
}×
[issue]
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023.
DOI fulltext PDF [bibtex]
@conference{PPVISII2023,
title = {Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants},
author = {Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {410-429},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_25},
url = { https://publications.rwth-aachen.de/record/957952},
}×
[issue]
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 410-429, Springer, 2023.
DOI fulltext PDF [bibtex]
@article{LBPDPP2023,
title = {Lower Bounds for Possibly Divergent Probabilistic Programs},
author = {Shenghua Feng and Mingshuai Chen and Han Su and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Naijun Zhan},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {7(OOPSLA1)},
pages = {pages 99},
type = {Journal Article},
year = {2023},
doi = {10.1145/3586051},
url = { https://publications.rwth-aachen.de/record/958360},
}×
[issue]
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan. Lower Bounds for Possibly Divergent Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA1), pages 99, ACM, 2023.
2022
DOI fulltext PDF [bibtex]
@conference{DPYRDVPPGF2022,
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},
}×
[issue]
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]
@article{ES2022,
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},
}×
[issue]
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