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.

Publications

Names marked ⁺ indicate equal contribution.

• 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
  OOPSLA 2025

• Refinement Types for Visualization
  Jingtao Xia⁺, Junrui Liu⁺, Nicholas Brown, Yanju Chen, Yu Feng
  ASE 2024

• 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
  S&P (Oakland) 2024

• Conflict-Driven Synthesis for Layout Engines
  Junrui Liu, Yanju Chen, Eric Atkinson, Yu Feng, Rastislav Bodik
  PLDI 2023

• Learning Contract Invariants Using Reinforcement Learning
  Junrui Liu⁺, Yanju Chen⁺, Bryan Tan, Isil Dillig, Yu Feng
  ASE 2022

• Tree Traversal Synthesis Using Domain-Specific Symbolic Compilation
  Yanju Chen, Junrui Liu, Yu Feng, Rastislav Bodik
  ASPLOS 2022

Preprints

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

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 @ Science of Blockchain Conference, Stanford University · Jul 2022

• Introduction to Interactive Theorem Proving in Coq
  0xPARC Summer Residency, NYC · Jul 2022

• Refinement Types and Program Verification
  Guest lecture for CS 162, UCSB · Feb 2022

Service

• Artifact Evaluation Committee
  PLDI 2026 · ECOOP 2026 · USENIX Security 2026

• External Reviewer
  ISSTA 2026 · USENIX Security 2026 · TSE 2024

• Student Volunteer
  PLDI 2022