Prof. Dr. Mingshuai Chen is a US-equivalent tenure-track Assistant Professor leading the Formal Verification Group at Zhejiang University. Prior to joining ZJU, he worked as a Postdoctoral Researcher at RWTH Aachen University and a Visiting Researcher at University of Oldenburg, both in Germany. He received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences in 2019. His primary research interest lies in formal verification and synthesis, broadly construed in mathematical logic and theoretical computer science.

Mingshuai Chen has published over thirty peer-reviewed papers at flagship journals/conferences including Inf. Compt., IEEE Trans. Automat. Contr., OOPSLA, CAV, FM, ASE, ASPLOS, IJCAR, TACAS, etc. He serves as the workshop chair of ICFEM 2025, the guest editor of Journal of Software, and co-chair of multiple forums at ChinaSoft 2024. He serves on the reviewer panel of AMS Mathematical Reviews and the program/review committees of OOPSLA 2026, TACAS 2026/2025, ATVA 2025, etc. He was the awardee of the Distinguished Paper Award at ATVA 2018, Best Paper Award at FMAC 2019, and the CAS-President Special Award in 2019 (1st awardee from ISCAS ever since its inception in 1985). Mingshuai Chen is the recipient of the NSFC Excellent Young Scientists Fund Program (Overseas) -- one of the most prestigious grants for young researchers across China, the ZJNSF Major Program, the CCF-Huawei Populus Grove Fund, and the National Key Research and Development Program (as a key participant). His research results have been partially applied in the verification of control programs of the Chinese lunar lander Chang’e-3 and the Chinese high-speed railway system.

Our research group aims to develop formal reasoning techniques for programs and hybrid discrete-continuous systems for ensuring the reliability and effectiveness of safety-critical software systems while pushing the limits of automation as far as possible. In general, we are interested in formal methods – the rigorous mathematical basis of computer science. Concrete research directions include (yet not limited to):

• Logical Aspects of Computer Science

• Formal Verification and Synthesis

• Programming Theory/Languages

• Model Checking and Theorem Proving

• Cyber-Physical Systems

• Probabilistic/Quantum Systems

• Verification Meets AI/ML

We are constantly on the hunt of self-motivated Postdocs, Ph.D./Master Students, and Research Assistants/Interns to join our group at ZJU. Check out the open positions in case you are interested.