Abstract
Quantum technology is advancing at an exceptional pace and holds the potential to transform numerous sectors on both national and global scales. As quantum systems become more sophisticated and widespread, ensuring their correctness becomes critically important. This highlights the pressing need for rigorous tools capable of analyzing and verifying their behavior. However, developing such verification tools poses significant challenges. Fundamental quantum phenomena—most notably superposition and entanglement—lead to program behaviors that differ radically from those in classical computing. These characteristics give rise to inherently probabilistic models and result in exponentially large state spaces, even for systems of modest complexity.
In this paper, we outline initial steps toward addressing these challenges by drawing on insights gained from the verification of classical systems within our community. We then present a roadmap for designing novel verification frameworks that adapt the strengths of classical methods—such as succinct property specification, precise fault detection, automation, and scalability—to the quantum setting.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Throughout the text, we illustrate the challenges encountered in verifying quantum circuits through examples. For clarity, these examples are simplified. Full technical details are beyond the scope of this document and can be found, for example, in [35].
- 2.
An amplitude generalizes the classical notion of probability. The square of the absolute value of a complex amplitude gives the corresponding probability. The use of complex numbers permits constructive and destructive interference, allowing for the cancellation of certain outcomes.
- 3.
To simplify notation, we may represent column vectors using their transposes.
- 4.
Again, we give a high-level description here. We refer, e.g., to [35] for the algorithm details.
References
Abdulla, P.A.: A symbolic approach to verifying quantum systems. Commun. ACM (2025). https://doi.org/10.1145/3725725
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)
Abdulla, P.A., et al.: Verifying quantum circuits with level-synchronized tree automata. Proc. ACM Program. Lang. 9(POPL), 923–953 (2025). https://doi.org/10.1145/3704868
Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_14
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–736. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_56
Abdulla, P., Haziza, F., Holík, L.: Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transfer 18(5), 495–516 (2015). https://doi.org/10.1007/s10009-015-0406-x
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–7 June 2018. EPTCS, vol. 287, pp. 1–21 (2018). https://doi.org/10.4204/EPTCS.287.1
Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)
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übeck, Germany, 6–10 March 2023, Proceedings. Lecture Notes in Computer Science, vol. 14000, pp. 181–198. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-27481-7_12
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
Burgholzer, L., Wille, R.: Advanced equivalence checking for quantum circuits. IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst. 40, 1810–1824 (2020)
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–177. Springer, Cham (2021)
Chen, T.F., Chen, Y.F., Jiang, J.H.R., Jobranová, S., Lengál, 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)
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
Chen, Y., Chung, K., Lengál, 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–22 July 2023, Proceedings, Part III. Lecture Notes in Computer Science, vol. 13966, pp. 139–153. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-37709-9_7
Chen, Y., Chung, K., Lengál, 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–1243 (2023). https://doi.org/10.1145/3591270
Chen, Y., Rümmer, 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–4 July 2023, Proceedings. Lecture Notes in Computer Science, vol. 14132, pp. 170–189. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-38499-8_10
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
D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Math. Struct. Comput. Sci. 16(3), 429–451 (2006)
Fang, W., Ying, M.: Symbolic execution for quantum error correction programs. Proc. ACM Program. Lang. 8(PLDI), 1040–1065 (2024)
Floyd, R.W.: Assigning meanings to programs. 19, 19–32 (1967)
Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). https://doi.org/10.1145/363235.363259
King, J.C.: Symbolic execution and program testing. 19(7) (1976). https://doi.org/10.1145/360248.360252
Kissinger, A., van de Wetering, J.: Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions. Quantum Sci. Technol. 7(4), 044001 (2022)
Mei, J., Bonsangue, M., Laarman, A.: Simulating quantum circuits by model counting. In: Computer Aided Verification. Springer, Cham (2024)
Mei, J., Coopmans, T., Bonsangue, M., Laarman, A.: Equivalence checking of quantum circuits by model counting. In: Automated Reasoning, pp. 401–421. Springer, Cham (2024)
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–99 (2016)
Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: International Static Analysis Symposium, pp. 270–282. Springer, Cham (2008)
Piribauer, J., Baier, C.: Partial and conditional expectations in Markov decision processes with integer weights. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 436–452. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17127-8_25
Sistla, M., Chaudhuri, S., Reps, T.: Symbolic quantum simulation with quasimodo. In: Enea, C., Lal, A. (eds.) Computer Aided Verification, pp. 213–225. Springer, Cham (2023)
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–444. IEEE (2021)
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
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–528 (2022)
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–30. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_5
Yanofsky, N.S., Mannucci, M.A.: Quantum Computing for Computer Scientists, 1st edn. Cambridge University Press, Cambridge (2008)
Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(6), 1–49 (2012)
Yu, N., Palsberg, J.: Quantum abstract interpretation. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 542–558 (2021)
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–7 (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2026 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Abdulla, P.A. et al. (2026). On the Verification of Quantum Circuits (Research Challenges and Opportunities). In: Bertrand, N., Dubslaff, C., Klüppelholz, S. (eds) Principles of Formal Quantitative Analysis. Lecture Notes in Computer Science, vol 15760. Springer, Cham. https://doi.org/10.1007/978-3-031-97439-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-031-97439-7_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-97438-0
Online ISBN: 978-3-031-97439-7
eBook Packages: Computer ScienceComputer Science (R0)