- Click to reveal
- Room 4230
- +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.
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.
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.
- Latticed Craig Interpolation with an Application to Probabilistic Programs (Intern, Zhiang Wu (HKUST))
- On ∞-Safety of Probabilistic Programs (MSc, May 2020)
- 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)
- 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)
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
- Verification & Synthesis of Time-Delayed Dynamics. Doctoral Dissertation Defence at ISCAS, Beijing, China, May 2019.
- 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)
- 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)
|[bibtex] [issue]||Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023.|
|[bibtex] [issue]||Kevin Batz, Mingshuai Chen, Sebastian Junges, , Joost-Pieter Katoen, . Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, Tools and Algorithms for the Construction and Analysis of Systems, Volume 13994 of LNCS, 2023.|
|[bibtex] [issue]||Shenghua Feng, Mingshuai Chen, Han Su, , 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.|
|[bibtex] [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] [issue]||Mingshuai Chen, Bai Xue, , Joost-Pieter Katoen. Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming, Information and computation 289 (A), pages 104965, Elsevier, 2022.,|