While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
This chapter introduces both the requirements and challenges for an efficient use of formal methods in quantum computing and the current most promising research directions. While the recent progress in quantum hardware opens the door for significant speedup in cryptography as well as additional key areas (biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of quantum programs is a challenge. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. The chapter also introduces several existing solutions for the formal verification of quantum compilation and the equivalence of quantum program runs. The vast majority of quantum algorithms are described within the context of the quantum co-processor model, i.e. an hybrid model where a classical computer controls a quantum co-processor holding a quantum memory.
Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.
Quantum computing is getting increasing interest from both academia and industry, and the quantum software landscape has been growing rapidly. The quantum software stack comprises quantum programs, implementing algorithms, and platforms like IBM Qiskit, Google Cirq, and Microsoft Q#, enabling their development. To ensure the reliability and performance of quantum software, various techniques for testing and analyzing it have been proposed, such as test generation, bug pattern detection, and circuit optimization. However, the large amount of work and the fact that work on quantum software is performed by several research communities, make it difficult to get a comprehensive overview of the existing techniques. In this work, we provide an extensive survey of the state of the art in testing and analysis of quantum software. We discuss literature from several research communities, including quantum computing, software engineering, programming languages, and formal methods. Our survey covers a wide range of topics, including expected and unexpected behavior of quantum programs, testing techniques, program analysis approaches, optimizations, and benchmarks for testing and analyzing quantum software. We create novel connections between the discussed topics and present them in an accessible way. Finally, we discuss key challenges and open problems to inspire future research.
Quantum computing, grounded in the principles of superposition and entanglement, has emerged as a revolutionary paradigm with the potential to outperform classical systems in specific computational tasks. This paper presents a comprehensive survey of the foundational concepts, algorithmic developments, hardware architectures, and programming ecosystems in quantum computing. We analyze the current progress in key application areas such as cryptography, machine learning, optimization, and quantum chemistry. Furthermore, we review recent advances between 2023 and 2025, including developments in fault-tolerant architectures and quantum error correction. The paper also discusses the significant technical challenges that hinder large-scale practical deployment, including qubit scalability, decoherence, and programming limitations. By synthesizing literature across disciplines, this review aims to provide a holistic understanding of the quantum computing landscape and outline critical directions for future research and integration with classical systems.
Quantum computing exploits the principles of quantum mechanics to perform computation by manipulating qubit states through sequences of quantum gates, known as quantum circuits. As quantum hardware continues to scale in both complexity and qubit count, conventional verification techniques quickly become computationally impractical, motivating the need for more advanced verification approaches. Formal methods, including theorem proving, model checking, and symbolic reasoning, offer systematic and mathematically rigorous techniques for verifying functional correctness, equivalence, and implementation, while enabling early detection of design errors. This review explores how formal methods are currently applied to the verification of quantum circuits, with a particular focus on barrier certificates, abstract interpretation, model checking, theorem proving, and emerging hybrid approaches. Examining the theoretical foundations and practical applications of these techniques, discussing their strengths, limitations, and comparative effectiveness through representative case studies, review hopes to provide a holistic understanding of the topic. Highlighting the open challenges and outlining promising directions for future research, the review aims to provide a roadmap towards more scalable and robust verification frameworks for quantum computing. For readers seeking deeper engagement, the review offers an extensive set of references to support further study and exploration.
Recent advances in Quantum Machine Learning (QML) bring together Quantum Computing and Machine Learning with the aim of enhancing the advantages of Machine Learning to solve problems efficiently. The properties of quantum systems (superposition, entanglement, etc.) to represent multiple states of information at once, QML can potentially offer significant advantages when solving complex high-dimensional (multidimensional) computational problems. This paper reviews the current state-of-art regarding QML in general through an organized compilation and assessment of selected studies recently published in scientific literature that were found via large electronic library catalogs based on peer-reviewed sources according to algorithms used, optimization approaches employed, and areas of applied study. This review provides comparative analyses of each selected studies for purposes of identifying major trends in QML research/practice as well as opportunities for methodological improvements and challenges still existing within QML. Finally, this review presents an overview of Quantum Computing and Quantum Data Encoding Principles utilized to translate Classical Data into Quantum States as a high-level evaluation of several popular Quantum Learning Algorithms (e.g., Quantum Neural Networks, Quantum Support Machines, and Variational Quantum Circuit). The survey describes the optimization strategies such as gradient based techniques, Bayesian Optimization and evolutionary techniques being used to improve the stability of the quantum machine learning (QML) training process. Then, it provides examples of application areas for such QML, where healthcare analytics, environmental modelling, manufacturing optimization and analysis of biologic data are included. The comparative review of the recent academic research has identified several limitations and challenges regarding the use of QML that researchers. Although QML is believed to be capable of solving complex computational problems, issues such as noise in hardware, limited numbers of qubits and scalability present significant challenges for researchers working with this type of machine learning application. Overall, it appears that this survey provides a broad overview of contemporary developments and future trends for developing high-performance quantum learning systems.