Reconciling high-level optimizations and low-level code in LLVM. - Juneyoung Lee; Chung-Kil Hur; Ralf Jung 002; Zhengyang Liu 003; John Regehr; Nuno P. Lopes (Proc. ACM Program. Lang., 2018)

Testing static analyses for precision and soundness. - Jubi Taneja; Zhengyang Liu 003; John Regehr (CGO, 2020)

Dataflow-based pruning for speeding up superoptimization. - Manasij Mukherjee; Pranav Kant; Zhengyang Liu 003; John Regehr (Proc. ACM Program. Lang., 2020)

Alive2: bounded translation validation for LLVM. - Nuno P. Lopes; Juneyoung Lee; Chung-Kil Hur; Zhengyang Liu 003; John Regehr (PLDI, 2021)

Synthesizing optimal collective algorithms. - Zixian Cai; Zhengyang Liu 003; Saeed Maleki; Madanlal Musuvathi; Todd Mytkowicz; Jacob Nelson 001; Olli Saarikivi (PPoPP, 2021)

Minotaur: A SIMD-Oriented Synthesizing Superoptimizer. - Zhengyang Liu 003; Stefan Mada; John Regehr (Proc. ACM Program. Lang., 2024)