{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:11:56Z","timestamp":1775790716273,"version":"3.50.1"},"reference-count":90,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"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":[[2023,6,6]]},"abstract":"<jats:p>\n            We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a\u2004\u200dtriple {\n            <jats:italic>P<\/jats:italic>\n            }\u202f\n            <jats:italic>C<\/jats:italic>\n            \u202f{\n            <jats:italic>Q<\/jats:italic>\n            } and the question is whether, given a set\n            <jats:italic>P<\/jats:italic>\n            of quantum states on the input of a circuit\n            <jats:italic>C<\/jats:italic>\n            , the set of quantum states on the output is equal to (or included in) a set\n            <jats:italic>Q<\/jats:italic>\n            . While this is not suitable to specify, e.g., functional correctness of a quantum circuit, it is sufficient to detect many bugs in quantum circuits. We propose a technique based on tree automata to compactly represent sets of quantum states and develop transformers to implement the semantics of quantum gates over this representation. Our technique computes with an algebraic representation of quantum states, avoiding the inaccuracy of working with floating-point numbers. 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, e.g., 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. In addition, our work establishes a connection between quantum program verification and automata, opening new possibilities to exploit the richness of automata theory and automata-based verification in the world of quantum computing.\n          <\/jats:p>","DOI":"10.1145\/3591270","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1218-1243","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":34,"title":["An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2872-0336","authenticated-orcid":false,"given":"Yu-Fang","family":"Chen","sequence":"first","affiliation":[{"name":"Academia Sinica, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3356-369X","authenticated-orcid":false,"given":"Kai-Min","family":"Chung","sequence":"additional","affiliation":[{"name":"Academia Sinica, 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, Czechia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8560-2147","authenticated-orcid":false,"given":"Jyun-Ao","family":"Lin","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5832-0867","authenticated-orcid":false,"given":"Wei-Lun","family":"Tsai","sequence":"additional","affiliation":[{"name":"Academia Sinica, Taiwan \/ National Taiwan University, Taiwan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0045-9594","authenticated-orcid":false,"given":"Di-De","family":"Yen","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2022. GMP: The GNU Multiple Precision Arithmetic Library. https:\/\/gmplib.org\/ \t\t\t\t  2022. GMP: The GNU Multiple Precision Arithmetic Library. https:\/\/gmplib.org\/"},{"key":"e_1_2_1_2_1","unstructured":"2022. The repository: Issue #200 (ZX-Checker produces invalid result). https:\/\/github.com\/cda-tum\/qcec\/issues\/200 \t\t\t\t  2022. The repository: Issue #200 (ZX-Checker produces invalid result). https:\/\/github.com\/cda-tum\/qcec\/issues\/200"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_8"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054107004929"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_47"},{"key":"#cr-split#-e_1_2_1_6_1.1","unstructured":"Dorit Aharonov. 2003. A Simple Proof that Toffoli and Hadamard are Quantum Universal. https:\/\/doi.org\/10.48550\/arxiv.quant-ph\/0301040 10.48550\/arxiv.quant-ph"},{"key":"#cr-split#-e_1_2_1_6_1.2","unstructured":"Dorit Aharonov. 2003. A Simple Proof that Toffoli and Hadamard are Quantum Universal. https:\/\/doi.org\/10.48550\/arxiv.quant-ph\/0301040"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_2_1_9_1","volume-title":"Formal Methods in Quantum Circuit Design. Ph. D. Dissertation","author":"Amy Matthew","unstructured":"Matthew Amy . 2019. Formal Methods in Quantum Circuit Design. Ph. D. Dissertation . University of Waterloo . Matthew Amy. 2019. Formal Methods in Quantum Circuit Design. Ph. D. Dissertation. University of Waterloo."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2573505"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40578-0_16"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-019-1666-5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/167088.167097"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature23474"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0205-y"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00084-3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394885.3431590"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2020.3032630"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/635499.635502"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1021\/acs.chemrev.8b00803"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7811406"},{"key":"e_1_2_1_26_1","unstructured":"Yu-Fang Chen Kai-Min Chung Ond\u0159ej Leng\u00e1l Jyun-Ao Lin Wei-Lun Tsai and Di-De Yen. 2023. An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report). arxiv:2301.07747. \t\t\t\t  Yu-Fang Chen Kai-Min Chung Ond\u0159ej Leng\u00e1l Jyun-Ao Lin Wei-Lun Tsai and Di-De Yen. 2023. An Automata-based Framework for Verification and Bug Hunting in Quantum Circuits (Technical Report). arxiv:2301.07747."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102244"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884860"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005111"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1098\/rspa.2017.0551"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"e_1_2_1_32_1","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. \t\t\t\t  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_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2791292"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.26421\/QIC6.1-6"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_3"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.01.024"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.287.5"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/EURDAC.1993.410627"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2017.35"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_17"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3456877"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2013.04.002"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462177"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/237814.237866"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99498-7_16"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-3_30"},{"key":"e_1_2_1_48_1","unstructured":"Kesha Hietala Robert Rand Shih-Han Hung Xiaodi Wu and Michael Hicks. 2019. Verified optimization in a quantum intermediate representation. arXiv preprint arXiv:1904.06319. \t\t\t\t  Kesha Hietala Robert Rand Shih-Han Hung Xiaodi Wu and Michael Hicks. 2019. Verified optimization in a quantum intermediate representation. arXiv preprint arXiv:1904.06319."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.vlsi.2019.10.004"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0219749905001067"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_7"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_12"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1068009.1068288"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193313.011"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/aab822"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-018-0072-4"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_2"},{"key":"e_1_2_1_59_1","volume-title":"Chuang","author":"Nielsen Michael A.","year":"2011","unstructured":"Michael A. Nielsen and Isaac L . Chuang . 2011 . Quantum Computation and Quantum Information: 10th Anniversary Edition (10th ed.). Cambridge University Press , USA. isbn:978-1-10-700217-3 Michael A. Nielsen and Isaac L. Chuang. 2011. Quantum Computation and Quantum Information: 10th Anniversary Edition (10th ed.). Cambridge University Press, USA. isbn:978-1-10-700217-3"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2459034"},{"key":"e_1_2_1_61_1","volume-title":"Pareto-Efficient Quantum Circuit Simulation Using Tensor Contraction Deferral. CoRR, abs\/1710.05867","author":"Pednault Edwin","year":"2017","unstructured":"Edwin Pednault , John A. Gunnels , Giacomo Nannicini , Lior Horesh , Thomas Magerlein , Edgar Solomonik , Erik W. Draeger , Eric T. Holland , and Robert Wisnieff . 2017. Pareto-Efficient Quantum Circuit Simulation Using Tensor Contraction Deferral. CoRR, abs\/1710.05867 ( 2017 ), arxiv:1710.05867 Edwin Pednault, John A. Gunnels, Giacomo Nannicini, Lior Horesh, Thomas Magerlein, Edgar Solomonik, Erik W. Draeger, Eric T. Holland, and Robert Wisnieff. 2017. Pareto-Efficient Quantum Circuit Simulation Using Tensor Contraction Deferral. CoRR, abs\/1710.05867 (2017), arxiv:1710.05867"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530480"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87744-8_60"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1994.365700"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2010.5491754"},{"key":"e_1_2_1_67_1","doi-asserted-by":"crossref","unstructured":"Lee Spector. 2006. Automatic Quantum Computer Programming: A Genetic Programming Approach. \t\t\t\t  Lee Spector. 2006. Automatic Quantum Computer Programming: A Genetic Programming Approach.","DOI":"10.1007\/978-0-387-36791-0"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785779"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2007.4397246"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-3065-8"},{"key":"e_1_2_1_72_1","volume-title":"Svore","author":"Wecker Dave","year":"2014","unstructured":"Dave Wecker and Krysta M . Svore . 2014 . LIQUi\u011brt > : A Software Design Architecture and Domain-Specific Language for Quantum Computing. CoRR , abs\/1402.4467 (2014), arXiv:1402.4467. arxiv:1402.4467 Dave Wecker and Krysta M. Svore. 2014. LIQUi\u011brt > : A Software Design Architecture and Domain-Specific Language for Quantum Computing. CoRR, abs\/1402.4467 (2014), arXiv:1402.4467. arxiv:1402.4467"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3489517.3530481"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISMVL.2008.43"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715261"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.01.044"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.26421\/QIC10.9-10-1"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527316"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_2"},{"key":"e_1_2_1_82_1","volume-title":"Model Checking Quantum Systems: Principles and Algorithms","author":"Ying Mingsheng","unstructured":"Mingsheng Ying and Yuan Feng . 2021. Model Checking Quantum Systems: Principles and Algorithms . Cambridge University Press . Mingsheng Ying and Yuan Feng. 2021. Model Checking Quantum Systems: Principles and Algorithms. Cambridge University Press."},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629680"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_21"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054111009112"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454061"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314584"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD45719.2019.8942057"},{"key":"e_1_2_1_89_1","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\/3591270","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591270","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591270"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":90,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591270"],"URL":"https:\/\/doi.org\/10.1145\/3591270","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}