Open Positions

We are constantly on the hunt of self-motivated Postdocs, Ph.D./Master Students, and Research Assistants/Interns to join our research group at ZJU.

About Hangzhou

As one of China’s most renowned and prosperous cities for much of the last millennium, Hangzhou has been long recognized as the “Paradise on Earth” – landmarked by West Lake. It is a major economic and e-commerce hub within China, and in particular, a major city for scientific research in the Asia-Pacific, ranking 23rd globally by scientific outputs. Hangzhou tops the list of Chinese cities of opportunity, for instance, Hangzhou is home to the headquarters of large global tech companies such as Alibaba Group, Ant Group, and NetEase.

Image credit: Unsplash

About Zhejiang University

As a member of the prestigious C9 League, Zhejiang University (founded as Qiushi Academy in 1897) is consistently ranked among the top 5 academic institutions in mainland China. As of 2022, the QS World University Rankings ranked Zhejiang University 42nd in the world and 5th in Asia. The ZJU College of Computer Science and Technology is committed to cultivating top-notch talents in computer science with cross-disciplinary innovation capabilities and global vision. The subjects it offers – Computer Science and Technology, and Software Engineering – are both rated A+ (2%, China University Subject Rankings).

Image credit: ZJU (Junjie Gao)

About the advisor

Prof. Dr. Mingshuai Chen is a ZJU100 Young 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, ASPLOS, IJGAR, TACAS etc. He serves in the reviewer panel of AMS Mathematical Reviews and the program/repeatability committees of TACAS 2025, FSEN 2025, RTCSA 2024/2021, SYNASC 2022, VMCAI 2021, ADHS 2021, etc. He was the awardee of the NSFC Excellent Young Scientists Fund Program (Overseas, one of the most prestigious grants for young researchers across China), 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). Part of his research results has been successfully applied in the verification of control programs of the Chinese lunar lander Chang’e-3 and the Chinese high-speed railway system.

Check out Mingshuai Chen’s CV for more detailed information.

Research topics

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 methods1 – 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

Check out Mingshuai Chen’s research statement for more details on these directions.

What do we expect?

  • Solid background in computer science, mathematics, software, control theory, or related areas. Knowledge in (a subset of) the following lectures is preferred:
    • Undergraduate level: Automata Theory, Compiler Construction, Programming Languages, Differential Equations, and Discrete Mathematics.
    • Graduate level: Mathematical Logic, Theory of Computation/Programming, Program Analysis/Verification, Formal Semantics, Model Checking, SAT/SMT Solving, Theorem Proving, Decision Procedures, Computer Algebra, Symbolic Computation, Game Theory, and Process Algebra.
    • Mathematics and Control: Algebra, Optimization, Probability Theory, Stochastic Processes, Differential Geometry, and Optimal Control.
  • Passion and endurance for solving challenging (mathematical) research problems.
  • Research experience in the above-mentioned topics is a plus, yet not a requisite (except for Postdoc applicants).

What you can expect?

Our overall goal of teaching and advising is to assist the students in developing interests and independent, critical thinking skills for approaching fundamental principles in theoretical computer science. We position ourselves as coaches and co-learners in an inclusive community consisting of the supervisor, the students, the colleagues, and the world around us. Check out Mingshuai Chen’s teaching statement for more details.

  • Research: We are committed to providing students with a pure, free scientific research environment. The supervisor is deeply involved in the student’s full-cycle research work ranging from literature review, topic assessment, effort allocation, theory development, paper writing, to result presentation. We provide regular seminars to keep track of cutting-edge research outcomes. We constantly enjoy assisting students to develop their immature, yet creative ideas into solid research results (which we took more like collaborations than mentor-and-mentees). As an example, one of our mentees had co-authored two CAV papers already by the first two years of his graduate program.
  • Collaborations and Exchange: We have been – and will continue to be – working on the aforementioned research topics in extensive collaborations with international research groups at, e.g., RWTH Aachen, Saarland, and Oldenburg in Germany; MIT, UNM, and CU Boulder in the US; DTU in Denmark; Radboud in the Netherlands; NTU in Singapore; ISCAS and PKU in China. We are keen to offer every Ph.D. student the opportunity of short/long-term exchange programs with one or more of these groups.
  • Wages: We got sufficient funding to offer competitive packages!

How to apply?

Drop us an email indicating the position(s) you are interested in while enclosing your CV and transcripts. Note that the Ph.D. position starting in September, 2024 has been closed.

  1. Formal methods have long been at the heart of computer science; there are 14 Turing Award Recipients – the most amongst all the sub-fields of computer science. ↩︎