{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:15:20Z","timestamp":1784837720523,"version":"3.55.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using\n                    <jats:italic toggle=\"yes\">level-synchronized tree automata<\/jats:italic>\n                    (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of\n                    <jats:italic toggle=\"yes\">choices<\/jats:italic>\n                    , which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for\n                    <jats:italic toggle=\"yes\">parameterized verification<\/jats:italic>\n                    , i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches.We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.\n                  <\/jats:p>","DOI":"10.1145\/3704868","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"923-953","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Verifying Quantum Circuits with Level-Synchronized Tree Automata"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6832-6611","authenticated-orcid":false,"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0498-7287","authenticated-orcid":false,"given":"Yo-Ga","family":"Chen","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6957-1651","authenticated-orcid":false,"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Brno, Czechia"},{"name":"Aalborg University, Aalborg, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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, Brno, Czechia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-4495-6539","authenticated-orcid":false,"given":"Fang-Yi","family":"Lo","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5832-0867","authenticated-orcid":false,"given":"Wei-Lun","family":"Tsai","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"Parosh Aziz Abdulla Yo-Ga Chen Yu-Fang Chen Luk\u00e1s Hol\u00edk Ondrej Leng\u00e1l Fang-Yi Lo Jyun-Ao Lin and Wei-Lun Tsai. 2024. Verifying Quantum Circuits with Level-Synchronized Tree Automata (artifact). https:\/\/doi.org\/10.5281\/zenodo.13957472 10.5281\/zenodo.13957472 https:\/\/doi.org\/10.5281\/zenodo.13957472 10.5281\/zenodo.13957472.","DOI":"10.5281\/zenodo.13957472"},{"key":"e_1_3_2_3_2","unstructured":"Parosh Aziz Abdulla Yo-Ga Chen Yu-Fang Chen Luk\u00e1s Hol\u00edk Ondrej Leng\u00e1l Jyun-Ao Lin Fang-Yi Lo and Wei-Lun Tsai. [n. d.]. Verifying Quantum Circuits with Level-Synchronized Tree Automata (Technical Report). arXiv:2410.18540 [cs.LO] https:\/\/doi.org\/https:\/\/arxiv.org\/abs\/2410.18540 arxiv.org\/abs\/2410.18540 ."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054107004929"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_3"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Matthew Amy . 2018. Towards Large-scale Functional Verification of Universal Quantum Circuits. In Proceedings 15th International Conference on Quantum Physics and Logic QPL 2018 Halifax Canada 3-7th June 2018 (EPTCS Vol. 287) Peter Selinger and Giulio Chiribella (Eds.). 1-21. https:\/\/doi.org\/10.4204\/EPTCS.287.1 10.4204\/EPTCS.287.1","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"MD SAJID ANIS Abby-Mitchell H\u00e9ctor Abraham et al. 2021. Qiskit: An Open-source Framework for Quantum Computing. https:\/\/doi.org\/10.5281\/zenodo.2573505 10.5281\/zenodo.2573505","DOI":"10.5281\/zenodo.2573505"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1666-5"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167097"},{"key":"e_1_3_2_12_2","volume-title":"Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions","author":"Bertot Yves","year":"2013","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1038\/nature23474"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55210-3_181"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0205-y"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-8_10"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2017.0551"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_2_24_2","unstructured":"Hubert Comon Max Dauchet R\u00e9mi Gilleron Florent Jacquemard Denis Lugiez Christof L\u00f6ding Sophie Tison and Marc Tommasi. 2008. Tree automata techniques and applications."},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005251"},{"key":"e_1_3_2_26_2","volume-title":"Automata Theory: An Algorithmic Approach","author":"Esparza Javier","year":"2023","unstructured":"Javier Esparza and Michael Blondin. 2023. Automata Theory: An Algorithmic Approach. MIT Press."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1142\/S012905411000743X"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0849-4_10"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3514355"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00982-2_38"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2010.11.015"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0326-7"},{"key":"e_1_3_2_37_2","first-page":"348","volume-title":"International conference on logic for programming artificial intelligence and reasoning","author":"Rustan K","year":"2010","unstructured":"K Rustan M Leino. 2010. Dafny: An automatic program verifier for functional correctness. In International conference on logic for programming artificial intelligence and reasoning. Springer, 348-370."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3458817.3476169"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"issue":"3","key":"e_1_3_2_40_2","first-page":"963","article-title":"Markov and Yaoyun Shi. 2008. Simulating quantum computation by contracting tensor networks","volume":"38","year":"2008","unstructured":"Igor L Markov and Yaoyun Shi. 2008. Simulating quantum computation by contracting tensor networks. SIAM J. Comput. 38, 3 (2008), 963-981.","journal-title":"SIAM J. Comput."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1103\/RevModPhys.92.015003"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2006.35"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aab822"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_22"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_11"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"Meghana Sistla Swarat Chaudhuri and Thomas W. Reps. 2023. Symbolic Quantum Simulation with Quasimodo. In Computer Aided Verification - 35th International Conference CAV 2023 Paris France July 17-22 2023 Proceedings Part III (Lecture Notes in Computer Science Vol. 13966) Constantin Enea and Akash Lal (Eds.). Springer 213-225. https:\/\/doi.org\/10.1007\/978-3-031-37709-9_11 10.1007\/978-3-031-37709-9_11","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45332-8_10"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.91.147902"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-32157-3_1"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530481"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2008.43"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715261"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.102.062612"},{"key":"e_1_3_2_61_2","first-page":"542","article-title":"Quantum abstract interpretation","author":"Yu Nengkun","year":"2021","unstructured":"Nengkun Yu and Jens Palsberg. 2021. Quantum abstract interpretation. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 542-558. https:\/\/doi.org\/10.1145\/ 3453483.3454061 10.1145\/ 3453483.3454061","journal-title":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","unstructured":"Li Zhou Nengkun Yu and Mingsheng Ying. 2019. An applied quantum Hoare logic. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. 1149-1162. https:\/\/doi.org\/10.1145\/3314221.3314584 10.1145\/3314221.3314584","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2018.2834427"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704868","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704868","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:28Z","timestamp":1770200248000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704868"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":62,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704868"],"URL":"https:\/\/doi.org\/10.1145\/3704868","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}