{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T14:06:01Z","timestamp":1776261961042,"version":"3.50.1"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22749-2_21","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:13:41Z","timestamp":1776258821000},"page":"419-439","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting"],"prefix":"10.1007","author":[{"given":"Wei-Jia","family":"Huang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Chareton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kai-Min","family":"Chung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min-Hsiu","family":"Hsieh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jingyi","family":"Mei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"Parosh\u00a0Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Luk\u00e1\u0161 Hol\u00edk, Ond\u0159ej Leng\u00e1l, Jyun-Ao Lin, Fang-Yi Lo, and Wei-Lun Tsai. Verifying quantum circuits with level-synchronized tree automata. Proc. ACM Program. Lang., 9(POPL), January 2025.","DOI":"10.1145\/3704868"},{"key":"21_CR2","unstructured":"Rajeev Acharya, Laleh Aghababaie-Beni, Igor Aleiner, Trond\u00a0I Andersen, Markus Ansmann, Frank Arute, Kunal Arya, Abraham Asfaw, Nikita Astrakhantsev, Juan Atalaya, et\u00a0al. Quantum error correction below the surface code threshold. arXiv preprint arXiv:2408.13687, 2024."},{"key":"21_CR3","unstructured":"Matthew Amy. Towards large-scale functional verification of universal quantum circuits. arXiv preprint arXiv:1805.06908, 2018."},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Matthew Amy. Complete equational theories for the sum-over-paths with unbalanced amplitudes. Electronic Proceedings in Theoretical Computer Science, 384:127\u2013141, August 2023.","DOI":"10.4204\/EPTCS.384.8"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Matthew Amy and Joseph Lunderville. Linear and non-linear relational analyses for quantum program optimization. Proceedings of the ACM on Programming Languages, 9(POPL):1072\u20131103, 2025.","DOI":"10.1145\/3704873"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Frank Arute, Kunal Arya, Ryan Babbush, Dave Bacon, Joseph\u00a0C. Bardin, Rami Barends, Rupak Biswas, Sergio Boixo, Fernando G. S.\u00a0L. Brandao, David\u00a0A. Buell, et\u00a0al. Quantum supremacy using a programmable superconducting processor. Nature, 574(7779):505\u2013510, 2019.","DOI":"10.1038\/s41586-019-1666-5"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Fabian Bauer-Marquart, Stefan Leue, and Christian Schilling. symQV: Automated symbolic verification of Quantum Programs. In Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker, editors, Formal Methods, pages 181\u2013198, Cham, 2023. Springer International Publishing.","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"Lukas Burgholzer and Robert Wille. 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":"21_CR9","doi-asserted-by":"crossref","unstructured":"Christophe Chareton, S\u00e9bastien Bardin, Fran\u00e7ois Bobot, Valentin Perrelle, and Beno\u00eet Valiron. An automated deductive verification framework for circuit-building quantum programs. In European Symposium on Programming, pages 148\u2013177. Springer International Publishing Cham, 2021.","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"21_CR10","doi-asserted-by":"crossref","unstructured":"Tian-Fu Chen, Jie-Hong\u00a0R. Jiang, and Min-Hsiu Hsieh. Partial equivalence checking of quantum circuits. In 2022 IEEE International Conference on Quantum Computing and Engineering (QCE), pages 594\u2013604, 2022.","DOI":"10.1109\/QCE53715.2022.00082"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ond\u0159ej Leng\u00e1l, Jyun-Ao Lin, and Wei-Lun Tsai. Autoq 2.0: From verification of quantum circuits to verification of quantum programs. In TACAS 2025, pages 87\u2013108. Springer, 2025.","DOI":"10.1007\/978-3-031-90660-2_5"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen, Kai-Min Chung, Ondrej Leng\u00e1l, Jyun-Ao Lin, and Wei-Lun Tsai. AutoQ: An automata-based quantum circuit verifier. In Constantin Enea and Akash Lal, editors, Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, volume 13966 of Lecture Notes in Computer Science, pages 139\u2013153. Springer, 2023.","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen, Kai-Min Chung, Ondrej Leng\u00e1l, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang., 7(PLDI):1218\u20131243, 2023.","DOI":"10.1145\/3591270"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen, Kai-Min Chung, Ond\u0159ej Leng\u00e1l, Jyun-Ao Lin, Wei-Lun Tsai, and Di-De Yen. An automata-based framework for verification and bug hunting in quantum circuits. Commun. ACM, 68(6):85\u201393, June 2025.","DOI":"10.1145\/3725728"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Yu-Fang Chen, Philipp R\u00fcmmer, and Wei-Lun Tsai. A theory of cartesian arrays (with applications in quantum circuit verification). In International Conference on Automated Deduction, pages 170\u2013189. Springer, 2023.","DOI":"10.1007\/978-3-031-38499-8_10"},{"key":"21_CR16","unstructured":"Alexandre Cl\u00e9ment, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Beno\u00eet Valiron. Lov-calculus: A graphical language for linear optical quantum circuits. arXiv preprint arXiv:2204.11787, 2022."},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and diagrammatics. New Journal of Physics, 13(4):043016, Apr 2011.","DOI":"10.1088\/1367-2630\/13\/4\/043016"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Bob Coecke and Aleks Kissinger. Picturing quantum processes. Cambridge University Press, Cambridge, United Kingdom, 2017.","DOI":"10.1017\/9781316219317"},{"key":"21_CR19","doi-asserted-by":"crossref","unstructured":"Ross Duncan and Simon Perdrix. Graph states and the necessity of euler decomposition. In Conference on Computability in Europe, pages 167\u2013177. Springer, 2009.","DOI":"10.1007\/978-3-642-03073-4_18"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Ross Duncan and Simon Perdrix. Rewriting measurement-based quantum computations with generalised flow. In International Colloquium on Automata, Languages, and Programming, pages 285\u2013296. Springer, 2010.","DOI":"10.1007\/978-3-642-14162-1_24"},{"key":"21_CR21","unstructured":"Richard\u00a0P Feynman, Albert\u00a0R Hibbs, and Daniel\u00a0F Styer. Quantum mechanics and path integrals. Courier Corporation, 2010."},{"key":"21_CR22","unstructured":"Daniel Gottesman. The heisenberg representation of quantum computers. arXiv preprint quant-ph\/9807006, 1998."},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, Chia-Shun Yeh, and Mingsheng Ying. Decision diagrams for symbolic verification of quantum circuits. In 2023 IEEE International Conference on Quantum Computing and Engineering (QCE), volume\u00a01, pages 970\u2013977. IEEE, 2023.","DOI":"10.1109\/QCE57702.2023.00111"},{"key":"21_CR24","unstructured":"Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, and Mingsheng Ying. Equivalence checking of parameterised quantum circuits. arXiv preprint arXiv:2404.18456, 2024."},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Xin Hong, Xiangzhen Zhou, Sanjiang Li, Yuan Feng, and Mingsheng Ying. A tensor network based decision diagram for representation of quantum circuits. ACM Transactions on Design Automation of Electronic Systems (TODAES), 27(6):1\u201330, 2022.","DOI":"10.1145\/3514355"},{"key":"21_CR26","unstructured":"Ali Javadi-Abhari, Matthew Treinish, Kevin Krsulich, Christopher\u00a0J. Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul\u00a0D. Nation, Lev\u00a0S. Bishop, Andrew\u00a0W. Cross, Blake\u00a0R. Johnson, and Jay\u00a0M. Gambetta. Quantum computing with Qiskit, 2024."},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A complete axiomatisation of the zx-calculus for clifford+t quantum mechanics. LICS \u201918, page 559\u2013568, New York, NY, USA, 2018. Association for Computing Machinery.","DOI":"10.1145\/3209108.3209131"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Aleks Kissinger and John van\u00a0de Wetering. PyZX: Large Scale Automated Diagrammatic Reasoning. In Bob Coecke and Matthew Leifer, editors, Proceedings 16th International Conference onQuantum Physics and Logic, Chapman University, Orange, CA, USA., 10-14 June 2019, volume 318 of Electronic Proceedings in Theoretical Computer Science, pages 229\u2013241. Open Publishing Association, 2020.","DOI":"10.4204\/EPTCS.318.14"},{"key":"21_CR29","unstructured":"Jialin Ma, Isuru Fernando, and Xin Chen. symengine: Interface to the \u2019SymEngine\u2019 Library, 2022. R package version 0.2.2."},{"key":"21_CR30","unstructured":"Jingyi Mei, Marcello Bonsangue, and Alfons Laarman. Simulating quantum circuits by model counting. In CAV 2024, (accepted for publication). Springer, 2024. Pre-print available at arXiv:2403.07197."},{"key":"21_CR31","doi-asserted-by":"crossref","unstructured":"Jingyi Mei, Tim Coopmans, Marcello Bonsangue, and Alfons Laarman. Equivalence checking of quantum circuits by model counting. In International Joint Conference on Automated Reasoning, pages 401\u2013421. Springer, 2024.","DOI":"10.1007\/978-3-031-63501-4_21"},{"key":"21_CR32","doi-asserted-by":"crossref","unstructured":"Jingyi Mei, Jan Martens, and Alfons Laarman. Disentangling the gap between quantum and# sat. In International Colloquium on Theoretical Aspects of Computing, pages 17\u201340. Springer, 2024.","DOI":"10.1007\/978-3-031-77019-7_2"},{"key":"21_CR33","doi-asserted-by":"crossref","unstructured":"Aaron Meurer, Christopher\u00a0P Smith, Mateusz Paprocki, Ond\u0159ej \u010cert\u00edk, Sergey\u00a0B Kirpichev, Matthew Rocklin, AMiT Kumar, Sergiu Ivanov, Jason\u00a0K Moore, Sartaj Singh, et\u00a0al. Sympy: symbolic computing in python. PeerJ Computer Science, 3:e103, 2017.","DOI":"10.7717\/peerj-cs.103"},{"key":"21_CR34","unstructured":"Michael\u00a0A. Nielsen and Isaac Chuang. Quantum computation and quantum information. Cambridge University Press, Cambridge, United Kingdom, 2002."},{"key":"21_CR35","doi-asserted-by":"crossref","unstructured":"Tom Peham, Lukas Burgholzer, and Robert Wille. Equivalence checking of parameterized quantum circuits: Verifying the compilation of variational quantum algorithms. In Proceedings of the 28th Asia and South Pacific Design Automation Conference, ASPDAC \u201923, page 702\u2013708, New York, NY, USA, 2023. Association for Computing Machinery.","DOI":"10.1145\/3566097.3567932"},{"key":"21_CR36","doi-asserted-by":"crossref","unstructured":"Nils Quetschlich, Lukas Burgholzer, and Robert Wille. MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing. Quantum, 2023. MQT Bench is available at https:\/\/www.cda.cit.tum.de\/mqtbench\/.","DOI":"10.22331\/q-2023-07-20-1062"},{"key":"21_CR37","unstructured":"J\u00e9rome Ricciardi, S\u00e9bastien Bardin, Christophe Chareton, and Beno\u00eet Valiron. Quantum circuit equivalence checking: A tractable bridge from unitary to hybrid circuits. In 3rd International Workshop on Services and Quantum Software, 2025."},{"key":"21_CR38","doi-asserted-by":"crossref","unstructured":"Meghana Sistla, Swarat Chaudhuri, and Thomas Reps. Symbolic quantum simulation with quasimodo. In International Conference on Computer Aided Verification, pages 213\u2013225. Springer, 2023.","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"21_CR39","unstructured":"Ryosuke Suzuki, Kenji Hashimoto, and Masahiko Sakai. Improvement of projected model-counting solver with component decomposition using sat solving in components. Technical report, Technical report, JSAI Technical Report, SIG-FPAI-103-B506, 2017."},{"key":"21_CR40","doi-asserted-by":"crossref","unstructured":"Yu\u00a0Tanaka. Exact non-identity check is nqp-complete. International Journal of Quantum Information, 8(05):807\u2013819, 2010.","DOI":"10.1142\/S0219749910006599"},{"key":"21_CR41","doi-asserted-by":"crossref","unstructured":"Renaud Vilmart. The structure of sum-over-paths, its consequences, and completeness for clifford. In Foundations of Software Science and Computation Structures, volume 12650, page 531, 2021.","DOI":"10.1007\/978-3-030-71995-1_27"},{"key":"21_CR42","doi-asserted-by":"crossref","unstructured":"Renaud Vilmart. Rewriting and completeness of sum-over-paths in dyadic fragments of quantum computing. Logical Methods in Computer Science, Volume 20, Issue 1, March 2024.","DOI":"10.46298\/lmcs-20(1:20)2024"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Chun-Yu Wei, Yuan-Hung Tsai, Chiao-Shan Jhang, and Jie-Hong\u00a0R Jiang. Accurate bdd-based unitary operator manipulation for scalable and robust quantum circuit verification. In Proceedings of the 59th ACM\/IEEE Design Automation Conference, pages 523\u2013528, 2022.","DOI":"10.1145\/3489517.3530481"}],"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-032-22749-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:13:52Z","timestamp":1776258832000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All data and code supporting the findings of this study are openly available in the repository\n                      \n                      . The repository contains the implementation, example inputs, and artifacts required to reproduce the experimental results reported in this paper.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability"}},{"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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}