Mingshuai Chen

Address

Room 4230
Ahornstraße 55
D-52074 Aachen

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

• Science of Computer Programming
• Formal Aspects of Computing
• Nonlinear Analysis: Hybrid Systems

Conferences & Workshops

• TACAS (2023, 2021)
• POPL (2023)
• ICALP (2022)
• SAFECOMP 2022
• CAV (2021, 2020)
• ADHS (2021, 2018)
• ECC (2021, 2016)
• FORMATS 2020
• HSCC 2020
• RTSS 2019
• EMSOFT 2019
• MEMOCODE 2018
• ATVA (2018, 2015)
• ICECCS 2017
• TIME 2016
• VSTTE 2016
• UTP 2016
• TASE (2022, 2015)
• Chaochen Zhou’s Festschrift

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)

Publications