Mingshuai Chen

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

Research

I develop formal verification and synthesis techniques for programs and hybrid discrete-continuous systems for ensuring the reliability and effectiveness of safety-critical cyber-physical systems, and aim to push 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 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

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)

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 = {TBD},
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 TBD, pages 104965, Elsevier, 2022.
DOI [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},
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, 34th International Conference on Computer Aided Verification (CAV22), Volume 13371 of LNCS, Springer, 2022.
2021
DOI fulltext PDF [bibtex]
@conference{SIBCDCP2021,
title = {Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12759, Theoretical Computer Science and General Issues},
pages = {443-466},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81685-8_21},
url = { https://publications.rwth-aachen.de/record/822586},
}×
[issue]
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming, 33rd International Conference on Computer-Aided Verification (CAV 2021), Volume 12759, Theoretical Computer Science and General Issues of LNCS, 443-466, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{LIAPP2021,
title = {Latticed $k$-Induction with an Application to Probabilistic Programs},
author = {Kevin Batz and Mingshuai Chen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12760},
pages = {524-549},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81688-9_25},
url = { https://publications.rwth-aachen.de/record/822587},
}×
[issue]
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. Latticed $k$-Induction with an Application to Probabilistic Programs, 33rd International Conference on Computer-Aided Verification (CAV 2021), Volume 12760 of LNCS, 524-549, Springer, 2021.
Show all