Research Interests

I’m interested in helping programmers build provably correct, efficient software, using techniques from programming languages and formal methods. To achieve this, I work on:

• developing program synthesizers that generate correct-by-construction software automatically
• formally verifying that existing software conforms to logical specifications
• designing domain-specific languages to make it easier to build reliable software for emerging domains.

Peer-Reviewed Publications

(+ indicates equal contribution)

• 【OOPSLA'25】 Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits. Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Luke Pearson, Yanju Chen, Yu Feng.

• 【ASE'24】 Refinement Types for Visualization. Jingtao Xia + Junrui Liu, Nicholas Brown, Yanju Chen, Yu Feng.

• 【S&P'24】 Certifying Zero-Knowledge Circuits with Refinement Types. Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan Tan, Jonathan Wang, Yi Sun, Luke Pearson, Anders Miltner, Isil Dillig, Yu Feng.

• 【PLDI'23】 Conflict-Driven Synthesis for Layout Engines. Junrui Liu, Yanju Chen, Eric Atkinson, Yu Feng, Rastislav Bodik.

• 【ASE'22】 Learning Contract Invariants Using Reinforcement Learning. Junrui Liu + Yanju Chen, Bryan Tan, Isil Dillig, Yu Feng.

• 【ASPLOS'22】 Tree Traversal Synthesis Using Domain-Specific Symbolic Compilation. Yanju Chen, Junrui Liu, Yu Feng, Rastislav Bodik.

Preprints

• A Study of HTTP/2’s Server Push Performance Potential. Rui Meireles, Junrui Liu, Peter Steenkiste.

Invited Talks

• Tessel: An Optimizing Compiler for Efficient Zero-Knowledge Circuits, The Science of Blockchain Conference, UC Berkeley (Aug. 2025)
• Polymorphism, Curry-Howard, and Program Verification, Guest Lecture for CS 162, UCSB (Feb. 2023)
• Formal Verification for Zero-Knowledge Proofs, Applied ZK Workshop @ The Science of Blockchain Conference, Stanford University (July 2022)
• Introduction to Interactive Theorem Proving in Coq, 0xPARC Summer Residency, NYC (July 2022)
• Refinement Types and Program Verification, Guest Lecture for CS 162, UCSB (Feb. 2022)

Services

• USENIX Security'26, Artifact Evaluation Committee
• TSE'24, External Reviewer
• PLDI'22, Student Volunteer