{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:01:55Z","timestamp":1757624515482,"version":"3.44.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031974380"},{"type":"electronic","value":"9783031974397"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"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-031-97439-7_16","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:19Z","timestamp":1756551859000},"page":"320-341","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["On the\u00a0Verification of\u00a0Quantum Circuits (Research Challenges and\u00a0Opportunities)"],"prefix":"10.1007","author":[{"given":"Parosh Aziz","family":"Abdulla","sequence":"first","affiliation":[]},{"given":"Yo-Ga","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Kai-Min","family":"Chung","sequence":"additional","affiliation":[]},{"given":"Luk\u00e1\u0161","family":"Hol\u00edk","sequence":"additional","affiliation":[]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[]},{"given":"Jyun-Ao","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Fang-Yi","family":"Lo","sequence":"additional","affiliation":[]},{"given":"Wei-Lun","family":"Tsai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A.: A symbolic approach to verifying quantum systems. Commun. ACM (2025). https:\/\/doi.org\/10.1145\/3725725","DOI":"10.1145\/3725725"},{"key":"16_CR2","unstructured":"Abdulla, P.A., et al.: An automata-based framework for quantum circuit verification. Presentation at PLanQC 2025, The Fifth International Workshop on Programming Languages for Quantum Computing (2025)"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., et al.: Verifying quantum circuits with level-synchronized tree automata. Proc. ACM Program. Lang. 9(POPL), 923\u2013953 (2025). https:\/\/doi.org\/10.1145\/3704868","DOI":"10.1145\/3704868"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-642-12002-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2010","unstructured":"Abdulla, P.A., Chen, Y.-F., Hol\u00edk, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158\u2013174. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_14"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1007\/978-3-540-71209-1_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PA Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Regular model checking without transducers (on efficient verification of parameterized systems). In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 721\u2013736. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_56"},{"issue":"5","key":"16_CR6","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s10009-015-0406-x","volume":"18","author":"P Abdulla","year":"2015","unstructured":"Abdulla, P., Haziza, F., Hol\u00edk, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transfer 18(5), 495\u2013516 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0406-x","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Amy, M.: Towards large-scale functional verification of universal quantum circuits. In: Selinger, P., Chiribella, G. (eds.) Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3\u20137 June 2018. EPTCS, vol. 287, pp. 1\u201321 (2018). https:\/\/doi.org\/10.4204\/EPTCS.287.1","DOI":"10.4204\/EPTCS.287.1"},{"key":"16_CR8","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"Bauer-Marquart, F., Leue, S., Schilling, C.: symQV: automated symbolic verification of quantum programs. In: Chechik, M., Katoen, J., Leucker, M. (eds.) Formal Methods - 25th International Symposium, FM 2023, L\u00fcbeck, Germany, 6\u201310 March 2023, Proceedings. Lecture Notes in Computer Science, vol. 14000, pp. 181\u2013198. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_12","DOI":"10.1007\/978-3-031-27481-7_12"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Burgholzer, L., Jimenez-Pastor, A., Larsen, K.G., Tribastone, M., Tschaikowski, M., Wille, R.: Forward and backward constrained bisimulations for quantum circuits using decision diagrams. ACM Trans. Quantum Comput. 6(2) (2025). https:\/\/doi.org\/10.1145\/3712711","DOI":"10.1145\/3712711"},{"key":"16_CR11","doi-asserted-by":"publisher","first-page":"1810","DOI":"10.1109\/TCAD.2020.3032630","volume":"40","author":"L Burgholzer","year":"2020","unstructured":"Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 40, 1810\u20131824 (2020)","journal-title":"IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Chareton, C., Bardin, S., Bobot, F., Perrelle, V., Valiron, B.: An automated deductive verification framework for circuit-building quantum programs. In: Yoshida, N. (ed.) ESOP. LNCS, vol. 12648, pp. 148\u2013177. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Chen, T.F., Chen, Y.F., Jiang, J.H.R., Jobranov\u00e1, S., Leng\u00e1l, O.: Accelerating quantum circuit simulation with symbolic execution and loop summarization. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design (ICCAD). IEEE\/ACM (2024)","DOI":"10.1145\/3676536.3676711"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Chen, Y.F., et al.: Autoq 2.0: from verification of quantum circuits to verification of quantum programs. In: Proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). ETAPS 2025. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_5","DOI":"10.1007\/978-3-031-90660-2_5"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Chen, Y., Chung, K., Leng\u00e1l, O., Lin, J., Tsai, W.: AutoQ: an automata-based quantum circuit verifier. In: Enea, C., Lal, A. (eds.) Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, 17\u201322 July 2023, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 139\u2013153. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37709-9_7","DOI":"10.1007\/978-3-031-37709-9_7"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Chen, Y., Chung, K., Leng\u00e1l, O., Lin, J., Tsai, W., Yen, D.: An automata-based framework for verification and bug hunting in quantum circuits. Proc. ACM Program. Lang. 7(PLDI), 1218\u20131243 (2023). https:\/\/doi.org\/10.1145\/3591270","DOI":"10.1145\/3591270"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Chen, Y., R\u00fcmmer, P., Tsai, W.: A theory of cartesian arrays (with applications in quantum circuit verification). In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, 1\u20134 July 2023, Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 170\u2013189. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_10","DOI":"10.1007\/978-3-031-38499-8_10"},{"key":"16_CR18","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"3","key":"16_CR19","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1017\/S0960129506005251","volume":"16","author":"E D\u2019Hondt","year":"2006","unstructured":"D\u2019Hondt, E., Panangaden, P.: Quantum weakest preconditions. Math. Struct. Comput. Sci. 16(3), 429\u2013451 (2006)","journal-title":"Math. Struct. Comput. Sci."},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Fang, W., Ying, M.: Symbolic execution for quantum error correction programs. Proc. ACM Program. Lang. 8(PLDI), 1040\u20131065 (2024)","DOI":"10.1145\/3656419"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. 19, 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"16_CR22","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"King, J.C.: Symbolic execution and program testing. 19(7) (1976). https:\/\/doi.org\/10.1145\/360248.360252","DOI":"10.1145\/360248.360252"},{"issue":"4","key":"16_CR24","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ac5d20","volume":"7","author":"A Kissinger","year":"2022","unstructured":"Kissinger, A., van de Wetering, J.: Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions. Quantum Sci. Technol. 7(4), 044001 (2022)","journal-title":"Quantum Sci. Technol."},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. In: Computer Aided Verification. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65633-0_25"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. In: Automated Reasoning, pp. 401\u2013421. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-63501-4_21"},{"issue":"1","key":"16_CR27","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1109\/TCAD.2015.2459034","volume":"35","author":"P Niemann","year":"2016","unstructured":"Niemann, P., Wille, R., Miller, D.M., Thornton, M.A., Drechsler, R.: Qmdds: efficient quantum function representation and manipulation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 35(1), 86\u201399 (2016)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: International Static Analysis Symposium, pp. 270\u2013282. Springer, Cham (2008)","DOI":"10.1007\/978-3-540-69166-2_18"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-030-17127-8_25","volume-title":"Foundations of Software Science and Computation Structures","author":"J Piribauer","year":"2019","unstructured":"Piribauer, J., Baier, C.: Partial and conditional expectations in Markov decision processes with integer weights. In: Boja\u0144czyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 436\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_25"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with quasimodo. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 213\u2013225. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37709-9_11"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Tsai, Y.H., Jiang, J.H.R., Jhang, C.S.: Bit-slicing the hilbert space: scaling up accurate quantum circuit simulation. In: Proceedings of the 58th ACM\/IEEE Design Automation Conference (DAC), pp. 439\u2013444. IEEE (2021)","DOI":"10.1109\/DAC18074.2021.9586191"},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Vinkhuijzen, L., Coopmans, T., Elkouss, D., Dunjko, V., Laarman, A.: LIMDD: a decision diagram for simulation of quantum computing including stabilizer states. Quantum 7, 1108 (2023). https:\/\/doi.org\/10.22331\/q-2023-09-11-1108","DOI":"10.22331\/q-2023-09-11-1108"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Wei, C.Y., Tsai, Y.H., Jhang, C.S., Jiang, J.H.R.: Accurate BDD-based unitary operator manipulation for scalable and robust quantum circuit verification. In: Proceedings of the 59th ACM\/IEEE Design Automation Conference (DAC), pp. 523\u2013528 (2022)","DOI":"10.1145\/3489517.3530481"},{"key":"16_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11817963_5","volume-title":"Computer Aided Verification","author":"M De Wulf","year":"2006","unstructured":"De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17\u201330. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_5"},{"key":"16_CR35","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813887","volume-title":"Quantum Computing for Computer Scientists","author":"NS Yanofsky","year":"2008","unstructured":"Yanofsky, N.S., Mannucci, M.A.: Quantum Computing for Computer Scientists, 1st edn. Cambridge University Press, Cambridge (2008)","edition":"1"},{"issue":"6","key":"16_CR36","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2049706.2049708","volume":"33","author":"M Ying","year":"2012","unstructured":"Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), 1\u201349 (2012)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 542\u2013558 (2021)","DOI":"10.1145\/3453483.3454061"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Zulehner, A., Hillmich, S., Wille, R.: How to efficiently handle complex values? Implementing decision diagrams for quantum computing. In: 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 1\u20137 (2019)","DOI":"10.1109\/ICCAD45719.2019.8942057"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T13:20:12Z","timestamp":1757424012000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}