| [1] | Jiqi Li, Jingyi Mei, Wang Fang, and Ji Guan. Formal verification of quantum ancilla safety. In Computer Aided Verification, CAV 2026, 2026. [ DOI ] |
| [2] | Ming Xu, Yihao Chen, and Ji Guan. Model checking matrix product states against linear chain logic. In Computer Aided Verification, CAV 2026, 2026. [ arXiv ] |
| [3] | Zihao Li, Ji Guan, and Mingsheng Ying. QSeqSim: A symbolic simulator for Qiskit while loops using sequential quantum circuits. In Formal Methods, FM 2026, Lecture Notes in Computer Science. Springer, 2026. [ DOI | http | arXiv ] |
| [4] | Ming Xu, Jingyi Mei, Ji Guan, Yuxin Deng, and Nengkun Yu. Checking continuous stochastic logic against quantum continuous-time Markov chains. Logical Methods in Computer Science, 21(4), 2025. [ DOI ] |
| [5] | Ji Guan, Yuan Feng, Andrea Turrini, and Mingsheng Ying. Measurement-based verification of quantum Markov chains. In Computer Aided Verification, CAV 2024, Lecture Notes in Computer Science. Springer, 2024. [ DOI | http ] |
| [6] | Qisheng Wang, Ji Guan, Junyi Liu, Zhicheng Zhang, and Mingsheng Ying. New quantum algorithms for computing quantum entropies and distances. IEEE Trans. Inf. Theory, 70(8):5653–5680, 2024. [ DOI ] |
| [7] | Jingzhe Guo, Huazhe Lou, Riling Li, Wang Fang, Junyi Liu, Peixun Long, Shenggang Ying, and Mingsheng Ying. isQ: Towards a practical software stack for quantum programming. IEEE Transactions on Quantum Engineering, 2023. [ DOI ] |
| [8] | Mingsheng Ying, Li Zhou, Yangjia Li, and Yuan Feng. A proof system for disjoint parallel quantum programs. Theor. Comput. Sci., 897:164–184, 2022. [ DOI | http ] Distinguished Paper Award at LICS 2022 |
| [9] | Yuxiang Peng, Mingsheng Ying, and Xiaodi Wu. Algebraic reasoning of quantum programs via non-idempotent kleene algebra. In PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 657–670. ACM, 2022. [ DOI | http ] |
| [10] | Junyi Liu, Li Zhou, Gilles Barthe, and Mingsheng Ying. Quantum weakest preconditions for reasoning about expected runtimes of quantum programs. In LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 4:1–4:13. ACM, 2022. [ DOI | http ] |
| [11] | Ji Guan and Nengkun Yu. A probabilistic logic for verifying continuous-time Markov chains. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Springer, 2022. [ DOI ] |
| [12] | Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, and Nengkun Yu. A quantum interpretation of bunched logic & quantum separation logic. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, pages 1–14. IEEE, 2021. [ DOI | http ] |
| [13] | Ming Xu, Jingyi Mei, Ji Guan, and Nengkun Yu. Model checking quantum continuous-time Markov chains. In 32nd International Conference on Concurrency Theory, CONCUR 2021, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. [ DOI ] |
| [14] | Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. Relational proofs for quantum programs. Proc. ACM Program. Lang., 4(POPL):21:1–21:29, 2020. [ DOI | http ] |
| [15] | Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang., 4(OOPSLA):150:1–150:29, 2020. [ DOI | http ] Distinguished Paper Award at OOPSLA 2020 |
| [16] | Li Zhou, Nengkun Yu, and Mingsheng Ying. An applied quantum hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 1149–1162. ACM, 2019. [ DOI | http ] |
| [17] | Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum hoare logic. In Computer Aided Verification - 31st International Conference, CAV 2019, volume 11562 of Lecture Notes in Computer Science, pages 187–207. Springer, 2019. [ DOI | http ] |
| [18] | Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. Quantitative robustness analysis of quantum programs. Proc. ACM Program. Lang., 3(POPL):31:1–31:29, 2019. [ DOI | http ] |
| [19] | Mingsheng Ying. Toward automatic verification of quantum programs. Formal Aspects Comput., 31(1):3–25, 2019. [ DOI | http ] |
| [20] | Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Quantum hoare logic. Arch. Formal Proofs, 2019, 2019. [ .html ] |
| [21] | Yangjia Li and Mingsheng Ying. Algorithmic analysis of termination problems for quantum programs. Proc. ACM Program. Lang., 2(POPL):35:1–35:29, 2018. [ DOI | http ] |
| [22] | Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. Invariants of quantum programs: characterisations and generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 818–832. ACM, 2017. [ DOI | http ] |
| [23] | Yangjia Li, Nengkun Yu, and Mingsheng Ying. Termination of nondeterministic quantum programs. Acta Informatica, 51(1):1–24, 2014. [ DOI | http ] |
| [24] | Mingsheng Ying, Nengkun Yu, Yuan Feng, and Runyao Duan. Verification of quantum programs. Sci. Comput. Program., 78(9):1679–1700, 2013. [ DOI | http ] |
| [25] | Mingsheng Ying and Yuan Feng. A flowchart language for quantum programming. IEEE Trans. Software Eng., 37(4):466–485, 2011. [ DOI | http ] |
| [26] | Mingsheng Ying. Floyd-hoare logic for quantum programs. ACM Trans. Program. Lang. Syst., 33(6):19:1–19:49, 2011. [ DOI | http ] |
| [27] | Mingsheng Ying and Yuan Feng. Quantum loop programs. Acta Informatica, 47(4):221–250, 2010. [ DOI | http ] |
| [28] | Yuan Feng, Runyao Duan, Zheng-Feng Ji, and Mingsheng Ying. Proof rules for the correctness of quantum programs. Theor. Comput. Sci., 386(1-2):151–166, 2007. [ DOI | http ] |
This file was generated by bibtex2html 1.99.