{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T10:42:21Z","timestamp":1770892941841,"version":"3.50.1"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T00:00:00Z","timestamp":1748476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"abstract":"<jats:p>\n            As quantum computing hardware advances, the demand for scalable, precise, and fully automated verification techniques for quantum circuits grows. This paper introduces a novel automata-based framework tailored for the verification of quantum circuits. In our approach, the problem is framed as a triple\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mo>{<\/mml:mo>\n                  <mml:mi>P<\/mml:mi>\n                  <mml:mo>}<\/mml:mo>\n                  <mml:mspace width=\"0.166667em\"\/>\n                  <mml:mi>C<\/mml:mi>\n                  <mml:mspace width=\"0.166667em\"\/>\n                  <mml:mo>{<\/mml:mo>\n                  <mml:mi>S<\/mml:mi>\n                  <mml:mo>}<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            and the question is whether, given a set\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>P<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            of quantum states on the input of a circuit\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>C<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , the set of quantum states on the output is equal to (or included in) a set\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>S<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            . Our framework leverages\n            <jats:italic>tree automata<\/jats:italic>\n            to compactly represent sets of quantum states and we develop transformers to implement the semantics of quantum gates over this representation. We implemented the proposed approach in a prototype tool and evaluated its performance against various benchmarks from the literature. The evaluation shows that our approach is quite scalable, for example, we managed to verify a large circuit with 40 qubits and 141,527 gates, or catch bugs injected into a circuit with 320 qubits and 1,758 gates, where all tools we compared with failed. Additionally, our work bridges quantum program verification and automata, opening new possibilities to exploit the richness of automata theory in quantum computing.\n          <\/jats:p>","DOI":"10.1145\/3725728","type":"journal-article","created":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T14:59:38Z","timestamp":1748530778000},"update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[{"name":"Academia Sinica, Institute of Information Science, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3356-369X","authenticated-orcid":false,"given":"Kai-Min","family":"Chung","sequence":"additional","affiliation":[{"name":"Academia Sinica, Institute of Information Science, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3038-5875","authenticated-orcid":false,"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Faculty of Information Technology, Brno, Czech Republic"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8560-2147","authenticated-orcid":false,"given":"Jyun-Ao","family":"Lin","sequence":"additional","affiliation":[{"name":"National Taipei University of Technology, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5832-0867","authenticated-orcid":false,"given":"Wei-Lun","family":"Tsai","sequence":"additional","affiliation":[{"name":"Academia Sinica, Institute of Information Science, Taipei, Taiwan"},{"name":"National Taiwan University, Graduate Institute of Electronics Engineering, Taipei, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0045-9594","authenticated-orcid":false,"given":"Di-De","family":"Yen","sequence":"additional","affiliation":[{"name":"Liverpool University, School of Electrical Engineering, Electronics and Computer Science, Liverpool, England, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,5,29]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_3_1_3_2","doi-asserted-by":"crossref","unstructured":"Amy M. Towards large-scale functional verification of universal quantum circuits. In Proceedings 15th Intern. Conf. on Quantum Physics and Logic Selinger P. and Chiribella G. (eds.) 2018) 1\u201321.","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1666-5"},{"key":"e_1_3_1_5_2","volume-title":"Proc. 25th Annual ACM Symp. on Theory of Computing","author":"Bernstein E.","unstructured":"Bernstein, E. and Vazirani, U. V. Quantum complexity theory. In Proc. 25th Annual ACM Symp. on Theory of Computing, ACM Kosaraju, S.R., Johnson, D.S., and Aggarwal, A."},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734106"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3394885.3431590"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_3_1_9_2","doi-asserted-by":"crossref","unstructured":"Chen T.-F. Jiang J.-H.R. and Hsieh M.-H. Partial equivalence checking of quantum circuits. In Proc. 2022 IEEE Intern. Conf. on Quantum Computing and Engineering (2022) 594\u2013604.","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"e_1_3_1_10_2","unstructured":"Chen Y. et al. AutoQ 2.0: From verification of quantum circuits to verification of quantum programs (technical report). (2024); https:\/\/arxiv.org\/abs\/2411.09121."},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_1_14_2","unstructured":"Comon H. et al. Tree automata techniques and applications (2008)."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2791292"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/2011679.2011685"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749905001067"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_7"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aab822"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530481"},{"key":"e_1_3_1_24_2","doi-asserted-by":"crossref","unstructured":"Wille R. et al. RevLib: An online resource for reversible functions and reversible circuits. In Proc. Intern. Symp. on Multi-Valued Logic (2008) 220\u2013225; http:\/\/www.revlib.org.","DOI":"10.1109\/ISMVL.2008.43"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_1_26_2","doi-asserted-by":"crossref","unstructured":"Yu N. and Palsberg J. Quantum abstract interpretation. In Proceedings of the 42nd ACM SIGPLAN Intern. Conf. on Programming Language Design and Implementation (2021) 542\u2013558.","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834427"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3725728","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3725728","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:57:04Z","timestamp":1750298224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3725728"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,29]]},"references-count":26,"alternative-id":["10.1145\/3725728"],"URL":"https:\/\/doi.org\/10.1145\/3725728","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,29]]},"assertion":[{"value":"2025-05-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"3725728"}}