yanju@ucsd.edu (copied) Google Scholar GitHub CV Some Deadlines
I am a postdoctoral scholar at University of California, San Diego working with Prof. Yufei Ding. I develop program synthesis and verification methods in which logical reasoning and learned models complement each other, so that programs, and the AI agents that increasingly write and run them, are correct by construction, efficient at scale, and easy to use.
I’ve recently earned a Ph.D. degree in Computer Science at University of California, Santa Barbara, advised by Prof. Yu Feng. Even earlier, I studied in Computer Science at Sun Yat-sen University, advised by Prof. Rong Pan.
(+ means equal contribution)
Deduction-Powered Program Synthesis
Synthesis turns what a user intends into a program that provably does it. I study how deduction and learning reinforce each other, whether deduction guides learning [CAV’20] or learning guides deductive search [OOPSLA’22a], including how a synthesizer can learn from its own failed attempts [PLDI’23a], so that synthesis scales to real domains such as data science [VLDB’19, FSE’19, ASE’24], compilers [ASPLOS’22] and smart contracts [OOPSLA’22b]. The same methods apply to AI agents, whose architectures can be synthesized and improved automatically instead of being designed by hand [arXiv’26b].
Trustworthy Agentic Programming
Natural language is becoming how we ask for software and instruct agents, so whether a program does what was meant is a first-class correctness problem that formal reasoning can address. A model’s output can be grounded in a program checked against the request [PLDI’22], and users, models and verifiers can supply examples [ASE’23], candidates or proofs [ASE’25]. Agent specifications are natural language; I give them a formal semantics so they can be audited [arXiv’26c], tested [arXiv’26e], enforced at runtime [arXiv’26f] and used to grant authority safely [arXiv’26d], and study their supply chain [arXiv’26a].
Verified and Performant Cryptographic and Blockchain Systems
Cryptographic and blockchain systems must be fast and cannot afford mistakes, so I want them both efficient and provably correct. Synthesis-aided compilation [OOPSLA’25] and explicit circuit layout [SBC’25] optimize zero-knowledge circuits without changing their meaning, and analyses find under-constrained [PLDI’23b] or unsound [USENIX Sec’24] circuits and semantically divergent virtual machines [NDSS’27]. On chain, this gives verified protocols [CCS’26] and execution layers [ePrint’24a, ePrint’24b], contracts whose state [S&P’22], loops [ASE’20] and invariants [ASE’22] are checked before deployment, behavior-preserving optimization [OOPSLA’22b] and attack synthesis to contain live incidents [CCS’24].
–
–
(PC - Program/Review Committee·AEC - Artifact Evaluation Committee·ERC - Extended Review Committee)
(F. - Fall·W. - Winter·S. - Spring·M. - Summer)