Naijun Zhan

Dr. Naijun Zhan is a Boya distinguished professor in the School of Computer Science at Peking University (since April 2024). He previously served as a research professor at the State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences, and was a research professor of the Chinese Academy of Sciences (since 2015). He received his PhD in computer science from ISCAS in 2000, and MSc/BSc degrees in computer science and mathematical logic from Nanjing University in 1996 and 1993. From 2001–2004, he worked at the Faculty of Mathematics and Informatics, University of Mannheim, Germany. He is a recipient of the Outstanding Youth Fund of the National Science Foundation of China (2016).

Research interests

• Formal techniques for the design of real-time and hybrid systems
• Program verification and automated theorem proving
• Modal and temporal logics
• Concurrent computation models
• Semantic foundations of component and object systems

Tools and resources

• MARS (Modeling, Analysis and Verification of hybrid Systems): download
• Theorem Prover for HHL: download
• High-speed Chinese train control system case study: download

Prospective students and postdocs

I am looking for motivated undergrads, grads (PhD and master), and postdocs interested in formal methods (automated reasoning & model checking), hybrid systems, and safety-critical software. If you would like to join the group, please feel free to get in touch.