{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:56:20Z","timestamp":1790927780659,"version":"4.1.0"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["25-18318S"],"award-info":[{"award-number":["25-18318S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["25-17934S"],"award-info":[{"award-number":["25-17934S"]}],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100017520","name":"FIT BUT","doi-asserted-by":"crossref","award":["FIT-S-23-8151"],"award-info":[{"award-number":["FIT-S-23-8151"]}],"id":[{"id":"10.13039\/501100017520","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100020950","name":"National Science and Technology Council","doi-asserted-by":"publisher","award":["NSTC 114-2221-E-027-044 -MY2"],"award-info":[{"award-number":["NSTC 114-2221-E-027-044 -MY2"]}],"id":[{"id":"10.13039\/501100020950","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Science and Technology Council","award":["NSTC 114-2119-M-001-002-"],"award-info":[{"award-number":["NSTC 114-2119-M-001-002-"]}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA2386-23-1-4107"],"award-info":[{"award-number":["FA2386-23-1-4107"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001869","name":"Academia Sinica","doi-asserted-by":"publisher","award":["AS-IV-114-M07"],"award-info":[{"award-number":["AS-IV-114-M07"]}],"id":[{"id":"10.13039\/501100001869","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Brno City Municipality","award":["Brno Ph.D. Talent"],"award-info":[{"award-number":["Brno Ph.D. Talent"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    We present the first fully automatic framework for verifying relational properties of\n                    <jats:italic toggle=\"yes\">parameterized quantum programs<\/jats:italic>\n                    , i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output correctness as well as equivalence. At the core of our approach is a new automata model, synchronized weighted tree automata (SWTAs), which compactly and precisely captures the infinite families of quantum states produced by parameterized programs. We introduce a class of transducers to model quantum gate semantics and develop composition algorithms for constructing transducers of parameterized circuits. Verification is reduced to functional inclusion or equivalence checking between SWTAs, for which we provide decision procedures. Our implementation demonstrates both the expressiveness and practical efficiency of the framework by verifying a diverse set of representative parameterized quantum programs with verification times ranging from milliseconds to seconds.\n                  <\/jats:p>","DOI":"10.1145\/3776712","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"2021-2050","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Parameterized Verification of Quantum Circuits"],"prefix":"10.1145","volume":"10","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"},{"name":"M\u00e4lardalen University, V\u00e4ster\u00e5s, Sweden"}],"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, Institute of Information Science, Taipei, Taiwan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2428-8547","authenticated-orcid":false,"given":"Michal","family":"He\u010dko","sequence":"additional","affiliation":[{"name":"Brno University of Technology, Faculty of Information Technology, Brno, Czech Republic"}],"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, Faculty of Information Technology, Brno, Czech Republic"},{"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, Faculty of Information Technology, Brno, Czech Republic"}],"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\/0000-0002-9926-0931","authenticated-orcid":false,"given":"Ramanathan S.","family":"Thinniyam","sequence":"additional","affiliation":[{"name":"Uppsala University, Uppsala, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3725725"},{"key":"e_1_3_2_3_2","article-title":"Parameterized Verification of Quantum Circuits (Technical Report)","author":"Abdulla Parosh Aziz","year":"2025","unstructured":"Parosh Aziz Abdulla, Yu-Fang Chen, Michal He\u010dko, Luk\u00e1\u0161 Hol\u00edk, Ond\u0159ej Leng\u00e1l, Jyun-Ao Lin, and Ramanathan Srinivasan Thinniyam. 2025. Parameterized Verification of Quantum Circuits (Technical Report). CoRR 2511.19897 (2025). arXiv:2511.19897 https:\/\/arxiv.org\/abs\/2511.19897","journal-title":"CoRR"},{"key":"e_1_3_2_4_2","volume-title":"AutoQ-Para repository","author":"Abdulla Parosh Aziz","year":"2025","unstructured":"Parosh Aziz Abdulla, Yu-Fang Chen, Michal He\u010dko, Luk\u00e1\u0161 Hol\u00edk, Ond\u0159ej Leng\u00e1l, Jyun-Ao Lin, and Ramanathan S. Thinniyam. 2025. AutoQ-Para repository. https:\/\/github.com\/VeriFIT\/AutoQ-Para"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704868"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_8_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\u201321. doi:10.4204\/EPTCS.287.1","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4916(72)90270-9"},{"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\u2019Art: 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\u2019Art: the calculus of inductive constructions. Springer Science & Business Media."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/305\/05215"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0055105"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_3_2_17_2","volume-title":"Computer Aided Verification, 12th International Conference, CAV 2025 (LNCS)","author":"Chen Kean","year":"2025","unstructured":"Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz, Steve Zdancewic, and Gushu Li. 2025. Verifying Fault-Tolerance of Quantum Error Correction Codes. In Computer Aided Verification, 12th International Conference, CAV 2025 (LNCS). Springer."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3676536.3676711"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-90660-2_7"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591270"},{"key":"e_1_3_2_23_2","first-page":"87","volume-title":"TACAS 2025","author":"Chen Yu-Fang","year":"2025","unstructured":"Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ond\u0159ej Leng\u00e1l, Jyun-Ao Lin, and Wei-Lun Tsai. 2025. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. In TACAS 2025. Springer, 87\u2013108."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3725728"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005111"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38499-8_10"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_3_2_28_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_29_2","unstructured":"Steven A Cuccaro Thomas G Draper Samuel A Kutin and David Petrie Moulton. 2004. A new quantum ripple-carry addition circuit. arXiv preprint quant-ph\/0410184 (2004)."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01492-5"},{"key":"e_1_3_2_31_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_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656419"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0849-4_10"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3514355"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729293"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ac5d20"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3458817.3476169"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1137\/050644756"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_25"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2006.35"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.5555\/1972505"},{"key":"e_1_3_2_49_2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume":"2283","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media.","journal-title":"Isabelle\/HOL: a proof assistant for higher-order logic"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.32.3266"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45332-8_10"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevLett.91.147902"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530481"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","unstructured":"Mingkuan Xu Zikun Li Oded Padon Sina Lin Jessica Pointing Auguste Hirth Henry Ma Jens Palsberg Alex Aiken Umut A Acar et al. 2022. Quartz: superoptimization of Quantum circuits. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 625\u2013640. doi:10.1145\/3519939.3523433","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","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\u2013558. doi:10.1145\/3453483.3454061","DOI":"10.1145\/3453483.3454061"},{"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\u20131162. doi: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\/pdf\/10.1145\/3776712","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:43:52Z","timestamp":1784209432000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776712"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":62,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776712"],"URL":"https:\/\/doi.org\/10.1145\/3776712","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}