I have been doing my Bachelor’s thesis at the Formal Verification Group under the supervision of Dr. Mingshuai Chen, where we aim to synthesize (possibly infinite-state) loopy probabilistic programs encoding randomized algorithms. I have also contributed to Parf - a framework for adaptively tuning external parameters of abstract interpretation-based static analyzers.

I am currently a Ph.D. candidate at the Polytechnic Institute of Zhejiang University.