My first research project was on verification-aided optimization. My colleagues and I implemented a deep-embedded version of VST, VST-A , and part of VST-Floyd in Coq. Then, we were able to use verified program annotation to guide the optimization pass, ensuring its soundness. In this project, I mainly worked on verified symbolic execution, which serves as a solid foundation of program correctness. This work will be covered in my bachelor's thesis, and I plan to submit it to a suitable conference in 2024.
My second project was an optimizing zero-knowledge circuit compiler. Zero-knowledge circuits are a relatively new computation model, and we are trying to fill the gap in optimizing compilers for it. I evaluated manual optimizations done by domain experts and designed an optimization-friendly FRP-style IR. We defined a cost-minimizing synthesizing problem on top of that, and it's still being actively worked on.
: https://arxiv.org/pdf/1909.00097.pdf, accepted to POPL'24
Designed by myself .
Last updated on 2023/12/15.