Non-preemptive Semantics for Data-Race-Free Programs. - Siyang Xiao; Hanru Jiang; Hongjin Liang 001; Xinyu Feng 001 (ICTAC, 2018)

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

Symbolic Reasoning About Quantum Circuits in Coq. - Wenjun Shi; Qinxiang Cao; Yuxin Deng; Hanru Jiang; Yuan Feng 001 (J. Comput. Sci. Technol., 2021)

On incorrectness logic for Quantum programs. - Peng Yan; Hanru Jiang; Nengkun Yu (Proc. ACM Program. Lang., 2022)

Approximate Relational Reasoning for Quantum Programs. - Peng Yan; Hanru Jiang; Nengkun Yu (CAV (3), 2024)

Qubit Recycling Revisited. - Hanru Jiang (Proc. ACM Program. Lang., 2024)

A Program Logic for Concurrent Randomized Programs in the Oblivious Adversary Model. - Weijie Fan; Hongjin Liang 001; Xinyu Feng 001; Hanru Jiang (ESOP (1), 2025)