Formal Verification of Quantum Algorithms Using Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (CAV (2), 2019)

Quantum Hoare Logic. - Junyi Liu 002; Bohua Zhan; Shuling Wang 003; Shenggang Ying; Tao Liu; Yangjia Li; Mingsheng Ying; Naijun Zhan (Arch. Formal Proofs, 2019)

Expected Runtime of Quantum Programs. - Junyi Liu 002; Li Zhou 013; Mingsheng Ying (CoRR, 2019)

Equivalence checking of quantum finite-state machines. - Qisheng Wang; Junyi Liu 002; Mingsheng Ying (J. Comput. Syst. Sci., 2021)

Quantum Algorithm for Fidelity Estimation. - Qisheng Wang; Zhicheng Zhang; Kean Chen; Ji Guan 001; Wang Fang 001; Junyi Liu 002; Mingsheng Ying (IEEE Trans. Inf. Theory, 2023)

CoqQ: Foundational Verification of Quantum Programs. - Li Zhou 013; Gilles Barthe; Pierre-Yves Strub; Junyi Liu 002; Mingsheng Ying (Proc. ACM Program. Lang., 2023)

New Quantum Algorithms for Computing Quantum Entropies and Distances. - Qisheng Wang; Ji Guan 001; Junyi Liu 002; Zhicheng Zhang; Mingsheng Ying (IEEE Trans. Inf. Theory, 2024)

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. - Junyi Liu 002; Li Zhou 013; Gilles Barthe; Mingsheng Ying (J. ACM, 2025)