Towards certified separate compilation for concurrent programs. - Hanru Jiang; Hongjin Liang 001; Siyang Xiao; Junpeng Zha; Xinyu Feng 001 (PLDI, 2019)

Modular Verification of SPARCv8 Code. - Junpeng Zha; Xin-Yu Feng 001; Lei Qiao 002 (J. Comput. Sci. Technol., 2020)

Verifying optimizations of concurrent programs in the promising semantics. - Junpeng Zha; Hongjin Liang 001; Xinyu Feng 001 (PLDI, 2022)