About Me |
|
I am a Member of Technical Staff at Axiom Math, where I work on a frontier large language model for mathematical problem-solving and software verification.
I am interested in the two directions between automated reasoning and machine learning: using formal methods to make what a model produces checkable, and using models to attack the search problems that have long limited synthesis and verification. My Ph.D. approached this from the symbolic side — studying how users can express their intent to a program synthesizer, and when and why synthesizers fail on a given problem. Previously, I was a Software Engineer at ByteDance, and an Applied Scientist on the Proof Platforms (P2) team within the Automated Reasoning Group at Amazon Web Services, where I worked on loop-invariant inference in CBMC and Kani and on verifying the Rust standard library. I completed my Ph.D. in Computer Science at the University of Wisconsin–Madison, advised by Loris D'Antoni, and my bachelor's degree in Computer Science in the Yao Class at Tsinghua University, advised by Giulio Chiribella. |
News |
I joined Axiom Math as a Member of Technical Staff! 2026 |
Kani: A Model Checker for Rust accepted at ASE 26! 2026 |
I defended my PhD thesis: Guarantees in Program Synthesis! June 2021 |
Publications |
|
Workshop |
Talks & Posters |
Service |
|
Computer Aided Verification (CAV) — Program Committee 2026 Static Analysis Symposium (SAS) — External Reviewer 2026 Verification, Model Checking, and Abstract Interpretation (VMCAI) — Program Committee 2024 Synthesis (SYNT) — Program Committee 2021 Formal Methods in Computer-Aided Design (FMCAD) — External Reviewer 2020 Programming Language Design and Implementation (PLDI) — Artifact Evaluation Committee 2019 |