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)

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},
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.
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, 33. 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, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12760 of LNCS, 524-549, Springer, 2021.
2020
DOI fulltext PDF [bibtex]
@article{I2020,
title = {Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control},
author = {Mingshuai Chen and Martin Fränzle and Yangjia Li and Peter N. Mosaad and Naijun Zhan},
publisher = {Springer},
journal = {Acta informatica},
volume = {58(5)},
pages = {pages 497-528},
type = {Journal Article},
year = {2020},
doi = {10.1007/s00236-020-00374-7},
url = { https://publications.rwth-aachen.de/record/783310},
}×
[issue]
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 58 (5), pages 497-528, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{LOCTA2020,
title = {Learning One-Clock Timed Automata},
author = {Jie An and Mingshuai Chen and Bohua Zhan and Naijun Zhan and Miaomiao Zhang},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078, Theoretical Computer Science and General Issues},
pages = {444-462},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_25},
url = { https://publications.rwth-aachen.de/record/787949},
}×
[issue]
Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning One-Clock Timed Automata, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 444-462, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{UTSVSDD2020,
title = {Unbounded-Time Safety Verification of Stochastic Differential Dynamics},
author = {Shenghua Feng and Mingshuai Chen and Bai Xue and Sriram Sankaranarayanan and Naijun Zhan},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {327-348},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_18},
url = { https://publications.rwth-aachen.de/record/794357},
}×
[issue]
Shenghua Feng, Mingshuai Chen, Bai Xue, Sriram Sankaranarayanan, Naijun Zhan. Unbounded-Time Safety Verification of Stochastic Differential Dynamics, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 327-348, Springer, 2020.