About Me

Hi There!

I’m a PhD candidate at the School of Software of Tsinghua University and a member of the Formal Verification Group. I’m supervised by Prof. Fei He. My research interests are automated program analysis and verification, and to develop both theoretical and practical tools for establishing software safety. I’m also interested in broad topics about programming languages and computational logics.

I graduated from the Department of Computer Science and Techonology of Tsinghua University. Previously, I have done researches on formally verified compiler for synchronous data-flow language (Lustre), and string constriants solving (check out our string solver OSTRICH!) under supervision of Shengyuan Wang and Zhilin Wu respectively.

For more information, you may take a look at my blog (it’s mainly in Chinese).

News

• Our paper on deadlock verification has been accepted by CAV’26!
• I’ll be giving a talk on data-driven termination and non-termination analysis at ISCAS.
• We have received the ICSE’26 Distinguished Paper Award!
• Our paper on termination condition inference has been accepted by ICSE’26!
• I’ll be giving a talk on concurrent program verification at Peking University.
• Our paper on probabilistic programming has been accepted by OOPSLA’25!
• Our paper on robustness checking has been accepted by ASPLOS’25! I’ll attend the conference located at Rotterdam in person.
• I am now qualified as a PhD candidate.
• Our paper on data-driven non-termination analysis has been accepted by ICSE’23! I’ll attend the conference located at Melbourne in person.
• I’ll be giving a talk on our POPL’22 work at ChinaSoft’21.
• Our paper on expanding first-order string theory to real-world regular expressions has been accepted by POPL’22!