{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:09:38Z","timestamp":1776305378897,"version":"3.50.1"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031906596","type":"print"},{"value":"9783031906602","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We present a\u00a0verifier of quantum programs called <jats:sc>AutoQ\u00a02.0<\/jats:sc>. Quantum programs extend quantum circuits (the domain of <jats:sc>AutoQ\u00a01.0<\/jats:sc>) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a\u00a0formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a\u00a0support for specifying loop invariants). We have successfully used <jats:sc>AutoQ\u00a02.0<\/jats:sc> to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the <jats:italic>repeat-until-success<\/jats:italic> (RUS) algorithm and the weak-measurement-based version of Grover\u2019s search algorithm. <jats:sc>AutoQ\u00a02.0<\/jats:sc> can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover\u2019s search, we were able to handle the case of 100 qubits in <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\sim $$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mo>\u223c<\/mml:mo>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula>20 minutes.<\/jats:p>","DOI":"10.1007\/978-3-031-90660-2_5","type":"book-chapter","created":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:37:57Z","timestamp":1746005877000},"page":"87-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["AutoQ\u00a02.0: From Verification of Quantum Circuits to Verification of Quantum Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3356-369X","authenticated-orcid":false,"given":"Kai-Min","family":"Chung","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3396-8427","authenticated-orcid":false,"given":"Min-Hsiu","family":"Hsieh","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8695-5689","authenticated-orcid":false,"given":"Wei-Jia","family":"Huang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8560-2147","authenticated-orcid":false,"given":"Jyun-Ao","family":"Lin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5832-0867","authenticated-orcid":false,"given":"Wei-Lun","family":"Tsai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Chen, Y.G., Chen, Y.F., Hol\u00edk, L., Leng\u00e1l, O., Lin, J.A., Lo, F.Y., Tsai, W.L.: Verifying quantum circuits with level-synchronized tree automata. Proceedings of the ACM on Programming Languages 9(POPL), 923\u2013953 (2025)","DOI":"10.1145\/3704868"},{"key":"5_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Chen, Y., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06015, pp. 158\u2013174. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_14, https:\/\/doi.org\/10.1007\/978-3-642-12002-2_14","DOI":"10.1007\/978-3-642-12002-2_14"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Aharonov, D.: A simple proof that Toffoli and Hadamard are quantum universal (2003). https:\/\/doi.org\/10.48550\/arxiv.quant-ph\/0301040, https:\/\/arxiv.org\/abs\/quant-ph\/0301040","DOI":"10.48550\/arxiv.quant-ph\/0301040"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice, Lecture Notes in Computer Science, vol. 10001. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6, https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. In: Quantum Physics and Logic (2018)","DOI":"10.4204\/EPTCS.287.1"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Andr\u00e9s-Mart\u00ednez, P., Heunen, C.: Weakly measured while loops: peeking at quantum states. Quantum Science and Technology 7(2), 025007 (feb 2022). https:\/\/doi.org\/10.1088\/2058-9565\/ac47f1, https:\/\/dx.doi.org\/10.1088\/2058-9565\/ac47f1","DOI":"10.1088\/2058-9565\/ac47f1"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Anticoli, L., Piazza, C., Taglialegne, L., Zuliani, P.: Towards quantum programs verification: From Quipper circuits to QPMC. In: Devitt, S.J., Lanese, I. (eds.) Reversible Computation - 8th International Conference, RC 2016, Bologna, Italy, July 7-8, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09720, pp. 213\u2013219. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40578-0_16, https:\/\/doi.org\/10.1007\/978-3-319-40578-0_16","DOI":"10.1007\/978-3-319-40578-0_16"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Baudin, P., Bobot, F., B\u00fchler, D., Correnson, L., Kirchner, F., Kosmatov, N., Maroneze, A., Perrelle, V., Prevosto, V., Signoles, J., Williams, N.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569","DOI":"10.1145\/3470569"},{"key":"5_CR9","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer Science & Business Media (2013)"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Bocharov, A., Roetteler, M., Svore, K.M.: Efficient synthesis of universal repeat-until-success quantum circuits. Phys. Rev. Lett. 114, 080502 (Feb 2015). https:\/\/doi.org\/10.1103\/PhysRevLett.114.080502, https:\/\/link.aps.org\/doi\/10.1103\/PhysRevLett.114.080502","DOI":"10.1103\/PhysRevLett.114.080502"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Bouajjani, A., Habermehl, P., Hol\u00edk, L., Touili, T., Vojnar, T.: Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Ibarra, O.H., Ravikumar, B. (eds.) Implementation and Applications of Automata, 13th International Conference, CIAA 2008, San Francisco, California, USA, July 21-24, 2008. Proceedings. Lecture Notes in Computer Science, vol.\u00a05148, pp. 57\u201367. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-70844-5_7, https:\/\/doi.org\/10.1007\/978-3-540-70844-5_7","DOI":"10.1007\/978-3-540-70844-5_7"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Boykin, P.O., Mor, T., Pulver, M., Roychowdhury, V.P., Vatan, F.: A new universal and fault-tolerant quantum basis. Inf. Process. Lett. 75(3), 101\u2013107 (2000). https:\/\/doi.org\/10.1016\/S0020-0190(00)00084-3, https:\/\/doi.org\/10.1016\/S0020-0190(00)00084-3","DOI":"10.1016\/S0020-0190(00)00084-3"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 40(9), 1810\u20131824 (2020)","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Programming Languages and Systems: 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27\u2013April 1, 2021, Proceedings 30. pp. 148\u2013177. Springer International Publishing (2021)","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Yoshida, N. (ed.) ESOP. Lecture Notes in Computer Science, vol. 12648, pp. 148\u2013177. Springer International Publishing, Cham (March 2021)","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Chen, T., Chen, Y., Jiang, J.R., Leng\u00e1l, O., Jobranov\u00e1, S.: Accelerating quantum circuit simulation with symbolic execution and loop summarization. In: Proc. of ICCAD\u201924. ACM (2024)","DOI":"10.1145\/3676536.3676711"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Chen, T., Jiang, J.R., Hsieh, M.: Partial equivalence checking of quantum circuits. In: 2022 IEEE International Conference on Quantum Computing and Engineering (QCE). pp. 594\u2013604 (2022). https:\/\/doi.org\/10.1109\/QCE53715.2022.00082","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"5_CR18","unstructured":"Chen, Y.F., Chung, K.M., Hsieh, M.H., Huang, W.J., Lengal, O., Lin, J.A., Tsai, W.L.: AutoQ 2.0: An automata-based quantum program verifier (TACAS artifact evaluation record). https:\/\/zenodo.org\/records\/14114791 (2024)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Chung, K.M., Leng\u00e1l, O., Lin, J.A., Tsai, W.L.: AutoQ: An automata-based quantum circuit verifier. In: International Conference on Computer Aided Verification. pp. 139\u2013153. Springer (2023)","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Chen, Y., Chung, K., Leng\u00e1l, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits. In: 44th ACM SIGPLAN Conference on Programming Language Design and Implementation\u2014PLDI\u201923. ACM (2023)","DOI":"10.1145\/3591270"},{"key":"5_CR21","unstructured":"Chen, Y.F., Leng\u00e1l, O., Tsai, W.L.: AutoQ\u00a02.0: An automata-based C++ tool for quantum program verification (Nov 2024), https:\/\/github.com\/alan23273850\/AutoQ\/tree\/tacas25"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Coecke, B., Duncan, R.: Interacting quantum observables: categorical algebra and diagrammatics. New Journal of Physics 13(4), 043016 (apr 2011). https:\/\/doi.org\/10.1088\/1367-2630\/13\/4\/043016","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05674, pp. 23\u201342. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2, https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14. pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"D\u2019Hondt, E., Panangaden, P.: Quantum weakest preconditions. Mathematical Structures in Computer Science 16(3), 429\u2013451 (2006)","DOI":"10.1017\/S0960129506005251"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Fang, W., Ying, M., Wu, X.: Differentiable quantum programming with unbounded loops. ACM Trans. Softw. Eng. Methodol. 33(1) (nov 2023). https:\/\/doi.org\/10.1145\/3617178, https:\/\/doi.org\/10.1145\/3617178","DOI":"10.1145\/3617178"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Feng, Y., Ying, M.: Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing 2(4), 1\u201343 (2021)","DOI":"10.1145\/3456877"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Feng, Y., Yu, N., Ying, M.: Model checking quantum Markov chains. J. Comput. Syst. Sci. 79(7), 1181\u20131198 (2013). https:\/\/doi.org\/10.1016\/j.jcss.2013.04.002, https:\/\/doi.org\/10.1016\/j.jcss.2013.04.002","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., Paskevich, A.: Why3-where programs meet provers. In: Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 22. pp. 125\u2013128. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Mathematical Aspects of Computer Science. pp. 19\u201332. Proceedings of Symposia in Applied Mathematics, AMS (1967), https:\/\/mathscinet.ams.org\/mathscinet\/article?mr=235771","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Miller, G.L. (ed.) Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996. pp. 212\u2013219. ACM (1996). https:\/\/doi.org\/10.1145\/237814.237866, https:\/\/doi.org\/10.1145\/237814.237866","DOI":"10.1145\/237814.237866"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: From pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G.J. (eds.) Computing and Software Science - State of the Art and Perspectives, Lecture Notes in Computer Science, vol. 10000, pp. 345\u2013373. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18, https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18","DOI":"10.1007\/978-3-319-91908-9_18"},{"key":"5_CR33","unstructured":"Hietala, K., Rand, R., Hung, S.H., Wu, X., Hicks, M.: Verified optimization in a quantum intermediate representation. arXiv preprint arXiv:1904.06319 (2019)"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259, https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"5_CR35","doi-asserted-by":"publisher","unstructured":"Hol\u00edk, L., Leng\u00e1l, O., Sim\u00e1cek, J., Vojnar, T.: Efficient inclusion checking on explicit and semi-symbolic tree automata. In: Bultan, T., Hsiung, P. (eds.) Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06996, pp. 243\u2013258. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_18, https:\/\/doi.org\/10.1007\/978-3-642-24372-1_18","DOI":"10.1007\/978-3-642-24372-1_18"},{"key":"5_CR36","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) Programming Languages and Systems - 8th Asian Symposium, APLAS 2010, Shanghai, China, November 28 - December 1, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06461, pp. 304\u2013311. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17164-2_21, https:\/\/doi.org\/10.1007\/978-3-642-17164-2_21","DOI":"10.1007\/978-3-642-17164-2_21"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science, vol.\u00a06355, pp. 348\u2013370. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20, https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: VATA: A library for efficient manipulation of non-deterministic tree automata. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 79\u201394. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_7"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, B., Wang, S., Ying, S., Liu, T., Li, Y., Ying, M., Zhan, N.: Formal verification of quantum algorithms using quantum Hoare logic. In: International conference on computer aided verification. pp. 187\u2013207. Springer (2019)","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"5_CR40","doi-asserted-by":"publisher","unstructured":"Mateus, P., Ramos, J., Sernadas, A., Sernadas, C.: Temporal Logics for Reasoning about Quantum Systems, p. 389-413. Cambridge University Press (2009). https:\/\/doi.org\/10.1017\/CBO9781139193313.011","DOI":"10.1017\/CBO9781139193313.011"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Paetznick, A., Svore, K.M.: Repeat-until-success: Non-deterministic decomposition of single-qubit unitaries. Quantum Info. Comput. 14(15-16), 1277-1301 (nov 2014)","DOI":"10.26421\/QIC14.15-16-2"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: International Static Analysis Symposium. pp. 270\u2013282. Springer (2008)","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"5_CR43","doi-asserted-by":"crossref","unstructured":"Unruh, D.: Quantum Hoare logic with ghost variables. In: 2019 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). pp. 1\u201313. IEEE (2019)","DOI":"10.1109\/LICS.2019.8785779"},{"key":"5_CR44","doi-asserted-by":"publisher","unstructured":"Wei, C.Y., Tsai, Y.H., Jhang, C.S., Jiang, J.H.R.: Accurate bdd-based unitary operator manipulation for scalable and robust quantum circuit verification. In: Proceedings of the 59th ACM\/IEEE Design Automation Conference. p. 523-528. DAC \u201922, Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3489517.3530481, https:\/\/doi.org\/10.1145\/3489517.3530481","DOI":"10.1145\/3489517.3530481"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings 21. pp. 33\u201338. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Xu, M., Fu, J., Mei, J., Deng, Y.: Model checking QCTL plus on quantum Markov chains. Theor. Comput. Sci. 913, 43\u201372 (2022). https:\/\/doi.org\/10.1016\/j.tcs.2022.01.044, https:\/\/doi.org\/10.1016\/j.tcs.2022.01.044","DOI":"10.1016\/j.tcs.2022.01.044"},{"key":"5_CR47","doi-asserted-by":"crossref","unstructured":"Xu, M., Li, Z., Padon, O., Lin, S., Pointing, J., Hirth, A., Ma, H., Palsberg, J., Aiken, A., Acar, U.A., et\u00a0al.: Quartz: superoptimization of quantum circuits. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 625\u2013640 (2022)","DOI":"10.1145\/3519939.3523433"},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Ying, M.: Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 33(6), 1\u201349 (2012)","DOI":"10.1145\/2049706.2049708"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. pp. 542\u2013558 (2021)","DOI":"10.1145\/3453483.3454061"},{"key":"5_CR50","doi-asserted-by":"crossref","unstructured":"Zhou, L., Barthe, G., Strub, P.Y., Liu, J., Ying, M.: Coqq: Foundational verification of quantum programs. Proceedings of the ACM on Programming Languages 7(POPL), 833\u2013865 (2023)","DOI":"10.1145\/3571222"},{"key":"5_CR51","doi-asserted-by":"crossref","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. pp. 1149\u20131162 (2019)","DOI":"10.1145\/3314221.3314584"},{"key":"5_CR52","doi-asserted-by":"publisher","unstructured":"Zhu, S., Hung, S.H., Chakrabarti, S., Wu, X.: On the principles of differentiable quantum programming languages. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 272-285. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3385412.3386011, https:\/\/doi.org\/10.1145\/3385412.3386011","DOI":"10.1145\/3385412.3386011"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90660-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T09:38:18Z","timestamp":1746005898000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90660-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906596","9783031906602"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90660-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}