Amy, M.: Towards large-scale functional verification of universal quantum circuits. Electron. Proc. Theor. Comput. Sci. 287, 1–21 (2019). https://doi.org/10.4204/eptcs.287.1
Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages (2012)
Chen, Y., Chung, K., Hsieh, M., Huang, W., Lengál, O., Lin, J., Tsai, W.: AutoQ 2.0: From verification of quantum circuits to verification of quantum programs. In: Gurfinkel, A., Heule, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, 3–8 May 2025, Proceedings, Part III. Lecture Notes in Computer Science, vol. 15698, pp. 87–108. Springer, Heidelberg (2025). https://doi.org/10.1007/978-3-031-90660-2_5
Gottesman, D.: The heisenberg representation of quantum computers. arXiv preprint quant-ph/9807006 (1998)
Gottesman, D.: The heisenberg representation of quantum computers. In: Group22: Proceedings of the XXII International Colloquium on Group Theoretical Methods in Physics. pp. 32–43. No. LA-UR-98-2848, International Press (1998)
Hein, M., Dür, W., Eisert, J., Raussendorf, R., den Nest, M.V., Briegel, H.J.: Entanglement in graph states and its applications (2006). https://arxiv.org/abs/quant-ph/0602096
Hein, M., Eisert, J., Briegel, H.J.: Multiparty entanglement in graph states. Phys. Rev. A 69(6) (2004). https://doi.org/10.1103/physreva.69.062311
Huang, Q., Zhou, L., Fang, W., Zhao, M., Ying, M.: Efficient formal verification of quantum error correcting programs. Proc. ACM Program. Lang. 9(PLDI), 190 (2025). https://doi.org/10.1145/3729293
Liu, J., et al.: Quantum hoare logic. Archive of Formal Proofs (2019). https://isa-afp.org/entries/QHLProver.html, Formal proof development
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information, 10th Anniversary Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9780511976667
Shor, P.W.: Scheme for reducing decoherence in quantum computer memory. Phys. Rev. A 52, R2493–R2496 (1995). https://doi.org/10.1103/PhysRevA.52.R2493. https://link.aps.org/doi/10.1103/PhysRevA.52.R2493
Steane, A.: Multiple-particle interference and quantum error correction. Proc. R. Soc. Lond. Ser. A: Math. Phys. Eng. Sci. 452(1954), 2551–2577 (1996). https://doi.org/10.1098/rspa.1996.0136
Sundaram, A., Rand, R., Singhal, K., Lackey, B.: Hoare meets heisenberg: a lightweight logic for quantum programs (2025). https://arxiv.org/abs/2101.08939
Team, T.R.: The Rocq proof assistant. https://rocq-prover.org/. Accessed 14 Mar 2025
The INQWIRE Developers: INQWIRE QuantumLib (2022). https://github.com/inQWIRE/QuantumLib
Unruh, D.: Quantum hoare logic with ghost variables. In: Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’19, pp. 1–13. IEEE Computer Society (2019). https://doi.org/10.1109/LICS.2019.8785779
Wu, A., Li, G., Zhang, H., Guerreschi, G.G., Xie, Y., Ding, Y.: Qecv: quantum error correction verification (2021)
Ying, M.: Floyd-hoare Logic for Quantum Programs. ACM Trans. Program. Lang. Syst. 33(6), 19 (2012). https://doi.org/10.1145/2049706.2049708
Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: Coqq: foundational verification of quantum programs. Proc. ACM Program. Lang. 7(POPL), 833–865 (2023)
Zhou, L., Yu, N., Ying, M.: An applied quantum Hoare logic. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’19, pp. 1149–1162. ACM (2019). https://doi.org/10.1145/3314221.3314584. https://opus.lib.uts.edu.au/bitstream/10453/140615/2/3314221.3314584.pdf
US