{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:26:33Z","timestamp":1768213593597,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_3","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:55Z","timestamp":1768202515000},"page":"44-57","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficiently Verifying Quantum Programs with\u00a0Few T Gates"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-4523-4619","authenticated-orcid":false,"given":"Youngchan","family":"Cho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6842-5505","authenticated-orcid":false,"given":"Robert","family":"Rand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. Electron. Proc. Theor. Comput. Sci. 287, 1\u201321 (2019). https:\/\/doi.org\/10.4204\/eptcs.287.1","DOI":"10.4204\/eptcs.287.1"},{"key":"3_CR2","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages (2012)"},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Chen, Y., Chung, K., Hsieh, M., Huang, W., Leng\u00e1l, 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\u20138 May 2025, Proceedings, Part III. Lecture Notes in Computer Science, vol. 15698, pp. 87\u2013108. Springer, Heidelberg (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_5","DOI":"10.1007\/978-3-031-90660-2_5"},{"key":"3_CR4","unstructured":"Gottesman, D.: The heisenberg representation of quantum computers. arXiv preprint quant-ph\/9807006 (1998)"},{"key":"3_CR5","unstructured":"Gottesman, D.: The heisenberg representation of quantum computers. In: Group22: Proceedings of the XXII International Colloquium on Group Theoretical Methods in Physics. pp. 32\u201343. No. LA-UR-98-2848, International Press (1998)"},{"key":"3_CR6","unstructured":"Hein, M., D\u00fcr, 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"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1103\/physreva.69.062311"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1145\/3729293"},{"key":"3_CR9","unstructured":"Liu, J., et al.: Quantum hoare logic. Archive of Formal Proofs (2019). https:\/\/isa-afp.org\/entries\/QHLProver.html, Formal proof development"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"3_CR11","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511976667","volume-title":"Quantum Computation and Quantum Information","author":"MA Nielsen","year":"2010","unstructured":"Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information, 10th Anniversary Cambridge University Press, Cambridge (2010). https:\/\/doi.org\/10.1017\/CBO9780511976667","edition":"10th Anniversar"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Shor, P.W.: Scheme for reducing decoherence in quantum computer memory. Phys. Rev. A 52, R2493\u2013R2496 (1995). https:\/\/doi.org\/10.1103\/PhysRevA.52.R2493. https:\/\/link.aps.org\/doi\/10.1103\/PhysRevA.52.R2493","DOI":"10.1103\/PhysRevA.52.R2493"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Steane, A.: Multiple-particle interference and quantum error correction. Proc. R. Soc. Lond. Ser. A: Math. Phys. Eng. Sci. 452(1954), 2551\u20132577 (1996). https:\/\/doi.org\/10.1098\/rspa.1996.0136","DOI":"10.1098\/rspa.1996.0136"},{"key":"3_CR14","unstructured":"Sundaram, A., Rand, R., Singhal, K., Lackey, B.: Hoare meets heisenberg: a lightweight logic for quantum programs (2025). https:\/\/arxiv.org\/abs\/2101.08939"},{"key":"3_CR15","unstructured":"Team, T.R.: The Rocq proof assistant. https:\/\/rocq-prover.org\/. Accessed 14 Mar 2025"},{"key":"3_CR16","unstructured":"The INQWIRE Developers: INQWIRE QuantumLib (2022). https:\/\/github.com\/inQWIRE\/QuantumLib"},{"key":"3_CR17","doi-asserted-by":"publisher","unstructured":"Unruh, D.: Quantum hoare logic with ghost variables. In: Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS \u201919, pp. 1\u201313. IEEE Computer Society (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785779","DOI":"10.1109\/LICS.2019.8785779"},{"key":"3_CR18","unstructured":"Wu, A., Li, G., Zhang, H., Guerreschi, G.G., Xie, Y., Ding, Y.: Qecv: quantum error correction verification (2021)"},{"issue":"6","key":"3_CR19","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2049706.2049708","volume":"33","author":"M Ying","year":"2012","unstructured":"Ying, M.: Floyd-hoare Logic for Quantum Programs. ACM Trans. Program. Lang. Syst. 33(6), 19 (2012). https:\/\/doi.org\/10.1145\/2049706.2049708","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: Coqq: foundational verification of quantum programs. Proc. ACM Program. Lang. 7(POPL), 833\u2013865 (2023)","DOI":"10.1145\/3571222"},{"key":"3_CR21","doi-asserted-by":"publisher","unstructured":"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 \u201919, pp. 1149\u20131162. ACM (2019). https:\/\/doi.org\/10.1145\/3314221.3314584. https:\/\/opus.lib.uts.edu.au\/bitstream\/10453\/140615\/2\/3314221.3314584.pdf","DOI":"10.1145\/3314221.3314584"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:57Z","timestamp":1768202517000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}