About Me

I am a first year Computer Science PhD student at Courant Institute of Mathematical Sciences, New York University, working with Prof. Joseph Tassarotti in the ACSys group.

My research interests lie broadly in formal verification, and I am currently working on crash-aware future-dependent linearizability verification using prophecy variables in Iris.

In the summer and fall of 2023, I was an intern in Prof. Xinyu Wang’s group at the University of Michigan, and worked on SMT-based automated bounded equivalence verification for SQL queries as a follow-up of the VeriEQL project.

I received my B.E. degree with honors from the University of Science and Technology of China in 2024. During my undergraduate study, I worked with Prof. Yu Zhang on foreign function interfaces of Go. My thesis is about Coq formalization of SQL query optimization rules, which is co-supervised by Prof. Yu Zhang and Prof. Xinyu Wang.