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

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

On ∞-Safety of Probabilistic Programs (MSc, May 2020)

Academic Services

Teaching Assistant

Trends in Computer-Aided Verification (Seminar) (B.Sc./M.Sc., RWTH Aachen, SS 22)
Concurrency Theory (M.Sc., RWTH Aachen, WS 21/22)
Trends in Computer-Aided Verification (Seminar) (B.Sc./M.Sc., RWTH Aachen, SS 21)
Probabilistic Programming (Seminar) (B.Sc./M.Sc., RWTH Aachen, WS 20/21)
Theoretical Foundations of the UML (M.Sc., RWTH Aachen, SS 20)
Theories of Programming (M.Sc., UCAS, WS 17/18, WS 18/19)

Committee Member

Reviewer Panel of Mathematical Reviews
Program Committee Member of SYNASC 2022 (Logic and Programming Track)
Program Committee Member of RTCSA 2021
Repeatability Evaluation Program Committee Member of ADHS 2021
Artifact Evaluation Committee Member of VMCAI 2021
Organization Committee Member of SSFM (2019, 2018)

External Reviewer

Journals

Conferences & Workshops

Honors & Awards

High-Impact Publication in CS by Chinese Researchers across from Springer Nature
Institute-Nomination for the CAS Excellent Doctoral Dissertation Award 2020
CAS-President Special Award 2019 (1st awardee since ISCAS’s inception in 1985)
Best Paper Award at FMAC 2019
Distinguished Paper Award at ATVA 2018
Selected Attendee of the 6th Heidelberg Laureate Forum

Selected Talks

Dissertation Defence

Verification & Synthesis of Time-Delayed Dynamics. Doctoral Dissertation Defence at ISCAS, Beijing, China, May 2019.

Tutorials

Taming Delays in Cyber-Physical Systems. ESWEEK, Shanghai, China, Oct. 2022. Tutorial co-presented with Naijun Zhan.
Formal Analysis, Verification and Design of Safety-Critical CPS. Video-cast. RTSS, Houston, USA, Dec. 2020. RTSS-HTD Tutorial co-presented with Lei Bu, Qixin Wang and Naijun Zhan.

Conferences, Workshops, Seminars & Visits

Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions, ISCAS Seminar, ISCAS, Beijing, China, Dec. 2022.
Lower Bounds for Possibly Divergent Probabilistic Programs, MOVES’ Colloquium at Schloss Dagstuhl, Saarbrücken, Germany, Apr. 2022 & ROCKS, Nijmegen, Netherlands, May 2022.
Latticed k-Induction with an Application to Probabilistic Programs. Information Sciences Seminar & Youth Forum, Peking University, Beijing, China, Oct. 2021 & ISCAS Seminar, ISCAS, Beijing, China, Dec. 2022.
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. Video-cast. Seminar on Cyber-Physical Systems, University of Southampton, Southampton, UK, Apr. 2021 & CAV, Los Angeles, USA, Jul. 2021.
On ∞-Safety of Stochastic Differential Dynamics. Video-cast. MOVES Seminar, RWTH Aachen University, Aachen, Germany, Apr. 2020 & CAV, Los Angeles, USA, Jul. 2020.
(In-)Variant Synthesis for Probabilistic Programs [Immature Idea]. MOVES’ Winter Colloquium at Kleinwalsertal, Kleinwalsertal, Austria, Feb. 2020.
Interpolation over Nonlinear Arithmetic – Towards Program Reasoning and Verification. PKU Seminar on Programming Languages, Peking University, Beijing, China, Sep. 2019 & MOVES Seminar, RWTH Aachen University, Aachen, Germany, Nov. 2019 & FACAS, La Falda, Córdoba, Argentina, Mar. 2022.
Taming Delays in Dynamical Systems – Unbounded Verification of Delay Differential Equations. CAV, New York City, USA, Jul. 2019.
Modelling · Verification · Synthesis – A Peek into the Blueprint of Hybrid Systems. RWTH Aachen University, Aachen & Technische Universität München, München, Germany, Oct. 2018.
What’s to Come is Still Unsure – Synthesizing Controllers Resilient to Delayed Interaction. ATVA, Los Angeles, USA, Oct. 2018 & CAP, Beijing, China, Sep. 2018 & MISSION@INVAP, San Carlos de Bariloche, Argentina, Feb. 2022.
Towards Delays in Dynamical and Control Systems – Verification & Synthesis. Universität des Saarlandes, Saarbrücken, Germany, Jul. 2016 & LEDS, Shanghai, China, Dec. 2016.
Validated Simulation-Based Verification of Delayed Differential Dynamics. FM, Limassol, Cyprus, Nov. 2016.
Computing Reachable Sets of Linear Vector Fields Revisited. ECC, Aalborg, Denmark, Jun. 2016.
A Two-Way Path between Formal and Informal Design of Embedded Systems. UTP & iFM, Reykjavík, Iceland, Jun. 2016.
HHL Prover: An Improved Interactive Theorem Prover for Hybrid Systems. ICFEM, Paris, France, Nov. 2015.
Decidability of the Reachability for a Family of Linear Vector Fields. ATVA, Shanghai, China, Oct. 2015.

Publications (till 2019)

Book Chapters

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.

Peer-Reviewed Journal Articles

Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, and Ting Gan. From model to implementation: A network-algorithm programming language. SCIENCE CHINA Information Sciences. 63(7): 172102 (2020).
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. 6(1): 19-39 (2019).
Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan. Reachability analysis for solvable dynamical systems. In IEEE Trans. Automat. Contr.. 63(7): 2003-2018 (2018).

Peer-Reviewed Conference Papers

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].
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).
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.
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 [corrected version]. In Proc. of FORMATS 2017, LNCS 10419, pp. 281-299.
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.
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.
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.
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.
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.

Publications (since 2020)

2023
[bibtex] @unpublished{EPIUGF2023, title = {Exact Probabilistic Inference Using Generating Functions}, author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen}, pages = {3 Seiten}, type = {Preprint}, year = {2023}, doi = {10.48550/arXiv.2302.00513}, url = { https://arxiv.org/abs/2302.00513}, }× [issue]	Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 3 Seiten, 2023. https://arxiv.org/abs/2302.00513
[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.
[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
[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.
[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

Mingshuai Chen