- Click to reveal
- Room 4230
- +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.
My research interests include
- formal verification of probabilistic programs
- modelling, verification and synthesis of hybrid systems
- reachability analysis
- interpolant/invariant synthesis
- 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 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.
- On ∞-Safety of Probabilistic Programs (MSc, May 2020)
- Theoretical Foundations of the UML (RWTH Aachen, SS 20)
- Theories of Programming (UCAS, WS 19/18)
Organizer & Volunteer
Conferences & Workshops
- FORMATS 2020
- CAV 2020
- HSCC 2020
- RTSS 2019
- EMSOFT 2019
- MEMOCODE 2018
- ATVA (2018, 2015)
- ADHS 2018
- ICECCS 2017
- TIME 2016
- VSTTE 2016
- UTP 2016
- ECC 2016
- TASE 2015
- Chaochen Zhou’s Festschrift
Honors & Awards
- CAS-President Special Award 2019
- 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.
- Formal Analysis, Verification and Design of Safety-Critical CPS. RTSS, Hong Kong, China, Dec. 2019. RTSS-HTD Tutorial co-presented with Lei Bu, Qixin Wang and Naijun Zhan.
Conferences, Seminars & Visits
- (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.
- 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.
- 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.
- 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).
- 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]||Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, Miaomiao Zhang. Learning One-Clock Timed Automata, The 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078 of LNCS, pages 444-462, Springer, 2020.|
|[bibtex]||Mingshuai Chen, , , , . Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control, Acta informatica , 2020.|