Dr. Mingshuai Chen

Check my current homepage at the Formal Verification Group at Zhejiang University.

Alumnus at the Institute of Software, Chinese Academy of Sciences
E-mail: chenms@ios.ac.cn Advisor: Prof. Dr. Naijun Zhan Co-advisor: Prof. Dr. Martin Fränzle

"Live as if you were to die tomorrow. Learn as if you were to live forever." ― MAHATMA GANDHI

Research Interests

Modelling · Verification · Synthesis of Hybrid Systems: Reachability Computation; Program Reasoning; Interpolant/Invariant Synthesis; Time-Delayed Systems

^new Tutorial @ RTSS 2019: Formal analysis, verification and design of safety-critical CPS.

Publications

[1] Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan (2019): Indecision and delays are the parents of failure - Taming them algorithmically by synthesizing delay-resilient control. Acta Informatica. Under minor revision.

[2] Jian Wang, Jie An, Mingshuai Chen, Naijun Zhan, Lulin Wang, Miaomiao Zhang, and Ting Gan (2019): From model to implementation: A network-algorithm programming language. SCIENCE CHINA Information Sciences. To appear.

[3] Mingshuai Chen, Jian Wang, Jie An, Bohua Zhan, Deepak Kapur, and Naijun Zhan (2019): NIL: Learning nonlinear interpolants. In Proc. of CADE 2019, Lecture Notes in Computer Science 11716, pp. 178-196. Extended version [typos in Theorem 1 & Table 2 corrected]. Slides.

[4] Shenghua Feng, Mingshuai Chen, Naijun Zhan, Martin Fränzle, and Bai Xue (2019): Taming delays in dynamical systems - Unbounded verification of delay differential equations. In Proc. of CAV 2019, Lecture Notes in Computer Science 11561, pp. 650-669. (Arfifact Evaluated). Slides.

[5] Martin Fränzle, Mingshuai Chen, and Paul Kröger (2019): In memory of Oded Maler: Automatic reachability analysis of hybrid-state automata. In ACM SIGLOG News, vol. 6, no. 1, pp. 19-39.

[6] Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan (2018): What's to come is still unsure - Synthesizing controllers resilient to delayed interaction. In Proc. of ATVA 2018, Lecture Notes in Computer Science 11138, pp. 56-74. (Distinguished Paper Award). Extended version. Slides.

[7] Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan (2017): Reachability analysis for solvable dynamical systems. In IEEE Trans. Automat. Contr., vol. 63, no. 7, pp. 2003-2018.

[8] Bai Xue, Peter N. Mosaad, Martin Fränzle, Mingshuai Chen, Yangjia Li, and Naijun Zhan (2017): Safe over- and under-approximation of reachable sets for delay differential equations [corrected version]. In Proc. of FORMATS 2017, Lecture Notes in Computer Science 10419, pp. 281-299.

[9] Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, and Naijun Zhan (2016): Validated simulation-based verification of delayed differential dynamics. In Proc. of FM 2016, Lecture Notes in Computer Science 9995, pp. 137-154. Extended version. Slides.

[10] Ting Gan, Liyun Dai, Bican Xia, Naijun Zhan, Deepak Kapur, and Mingshuai Chen (2016): Interpolant synthesis for quadratic polynomial inequalities and combination with EUF [typos in Table 1 corrected]. In Proc. of IJCAR 2016, Lecture Notes in Computer Science 9706, pp. 195-212. Slides.

[11] Mingshuai Chen, Anders P. Ravn, Shuling Wang, Mengfei Yang, and Naijun Zhan (2016): A two-way path between formal and informal design of embedded systems. In Proc. of UTP 2016, Lecture Notes in Computer Science 10134, pp. 65-92. Extended version. Slides.

[12] Ting Gan, Mingshuai Chen, Yangjia Li, Bican Xia, and Naijun Zhan (2016): Computing reachable sets of linear vector fields revisited. In Proc. of ECC 2016, IEEE-Xplore, pp. 419-426. Slides.

[13] Ting Gan, Mingshuai Chen, Liyun Dai, Bican Xia, and Naijun Zhan (2015): Decidability of the reachability for a family of linear vector fields. In Proc. of ATVA 2015, Lecture Notes in Computer Science 9364, pp. 482-499. Slides.

[14] Mingshuai Chen, Xiao Han, Tao Tang, Shuling Wang, Mengfei Yang, Naijun Zhan, Hengjun Zhao, and Liang Zou (2015): 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.

Tools and Case Studies

NIL: a learning-based tool in Mathematica that is dedicated to synthesizing nontrivial (reverse) Craig interpolants for the quantifier-free theory of nonlinear arithmetic.
UDDER: a prototype in Mathematica that is committed to reducing the verification problem of exponentially stable DDEs over an unbounded temporal horizon to that over a bounded one.
CAV19-AE: the repeatability package for the artifact evaluation of CAV 2019.
NLFIntp: an online tool for synthesizing nonlinear interpolants.
DGame: a procedure in Mathematica which synthesizes controllers for safety games under delayed information. It declares either WINNING associated with a finite-memory winning strategy if the game is controllable, or LOSING otherwise with a delay under which the winning strategy vanishes.
DDEChecker: a prototype in Matlab which takes a specific time-bounded safety verification problem of delayed dynamical systems as input, and declares either SAFE if the over-approximation of the trajectories are proven not to reach the unsafe set, UNSAFE associated with a counterexample, or UNKNOWN otherwise. HySAT is further going to serve as an optimization kernel of this tool.
InterCQI: a prototype in Mathematica which synthesizes interpolants for concave quadratic polynomial inequalities as well as their combination with EUFs. To deal with SOS decomposition and SDP, the tool AiSat and solver CSDP are invoked.
MPPs: a procedure in Maple for discovering non-terminating inputs (NTI) for multi-path polynomial programs with equality conditions.
MARS: a toolchain for Modeling, Analyzing and veRifying hybrid Systems, which integrates Sim2HCSP, H2S, HHLProver, QEInvGenerator, and SOSInvGenerator, as well as a cases tudy on a descent guidance control program of a lunar lander (abbrev. HCS).
SOSInv: an SOS-based generator in Mathematica & Matlab that assists theorem prover to derive invariant for safety verification of hybrid systems, associating with a case study on a descent guidance control program of a lunar lander.
LinR: an efficient prototype in Mathematica which conducts reachability verification of linear differential systems, including input files respectively for dReach, HSolver, and flow* for three examples.
H2S: a fully automatic translator in C++ that interprets HCSP processes into Simulink diagrams, where a case study on a descent guidance control program of a lunar lander is associated.