I am a Ph.D. student in the NetVerify Lab at Xi’an Jiaotong University, advised by Prof. Peng Zhang. My research focuses on advancing formal methods from scalable and practical perspectives. I design a data structure to accelerate multi-round and incremental SMT solving, which has been successfully applied to access control policy analysis (AccessRefinery, FSE 2026). Moreover, I study how to efficiently encode network configurations as SMT constraints, thereby accelerating network verification (VeriBoost, FM 2026). Besides, I also work on mining network specifications to help operators automatically write verification targets (NetMiner, ICNP 2023; NetMiner, TON 2025). Outside of research, I enjoy playing badminton and swimming, and I enjoy discussing academic topics with others. I am in the job market (Spring 2026); feel free to contact me!