Abstract The rapid progress of quantum technologies, fostered by the efforts of both academia and industry, has stimulated the design of quantum programming languages and the development of methods to support their verification and optimization. As in the classical setting, static analysis plays a fundamental role in such an endeavour. In this paper, we provide a survey on static analysis approaches for quantum programs, which have been proposed in the literature, distinguishing between dataflow-oriented approaches, which are based on a graph representation of the program information flow, and domain-oriented approaches, which essentially consist of the definition of some appropriate abstract domains representing the program property to be analysed. To illustrate these two perspectives concretely, we also present in detail two specific analyses: a dataflow analysis for managing quantum variables and uncomputation, and a static analysis based on abstract interpretation for detecting state entanglement.
Quantum entanglement plays an important role in quantum computation and communication. It is necessary for many protocols and computations, but causes unexpected disturbance of computational states. Hence, static analysis of quantum entanglement in quantum programs is necessary. Several papers studied the problem. They decided qubits were entangled if multiple qubits unitary gates are applied to them, and some refined this reasoning using information about the state of each separated qubit. However, they do not care about the fact that unitary gate undoes entanglement and that measurement may separate multiple qubits. In this paper, we extend prior work using stabilizer formalism. It refines reasoning about separability of quantum variables in quantum programs.
The emergence of quantum computing raises the question of how to identify (security-relevant) programming errors during development. However, current static code analysis tools fail to model information specific to quantum computing. In this paper, we identify this information and propose to extend classical code analysis tools accordingly. Among such tools, we identify the Code Property Graph to be very well suited for this task as it can be easily extended with quantum computing specific information. For our proof of concept, we implemented a tool which includes information from the quantum world in the graph and demonstrate its ability to analyze source code written in Qiskit and OpenQASM. Our tool brings together the information from the classical and quantum world, enabling analysis across both domains. By combining all relevant information into a single detailed analysis, this powerful tool can facilitate tackling future quantum source code analysis challenges.
Static analysis is the process of analyzing software code without executing the software. It can help find bugs and potential problems in software that may only appear at runtime. Although many static analysis tools have been developed for classical software, due to the nature of quantum programs, these existing tools are unsuitable for analyzing quantum programs. This paper presents QChecker, a static analysis tool that supports finding bugs in quantum programs in Qiskit. QChecker consists of two main modules: a module for extracting program information based on abstract syntax tree (AST), and a module for detecting bugs based on patterns. We evaluate the performance of QChecker using the Bugs4Q benchmark. The evaluation results show that QChecker can effectively detect various bugs in quantum programs.
Classical program analysis techniques, such as abstract interpretation and symbolic execution, are essential for ensuring software correctness, optimizing performance, and enabling compiler optimizations. However, these techniques face computational limitations when analyzing programs with large or exponential state spaces, limiting their effectiveness in ensuring system reliability. Quantum computing, with its parallelism and ability to process superposed states, offers a promising solution to these challenges. In this work, we present
QEX, a design that uses quantum computing to analyze classical programs. By synthesizing quantum circuits that encode program states in superposition and trace data dependency between program variables through entanglement,
QEXenables the simultaneous exploration of program behaviors, significantly improving scalability and precision. This advancement has broad applications, from debugging and security verification to optimizing compilers for next-generation hardware. As a proof-of-concept, we evaluated QEX on 22 benchmark programs, demonstrating its effectiveness in analyzing program states. To support more language features and make
QEXrealized sooner in Fault-Tolerant Quantum Computing (FTQC), we propose
QEX−Hwhich hybridizes QEX with classical analysis techniques. To our knowledge, this work is the first proposal to use quantum computing for classical program analysis.
Quantum computing operates in a fundamentally different way from classical computing by harnessing the principles of quantum mechanics to process information. Quantum supremacy is achieved when a quantum computer can solve problems that are beyond the capabilities of classical systems, including the human brain, showcasing its superior processing power. To attain quantum supremacy, quantum entanglement and qubit interactions play a pivotal role. Quantum entanglement occurs when qubits are interconnected in a manner where the state of one qubit directly influences the state of others, enabling the quantum computer to perform multiple operations simultaneously. Moreover, effective interaction between qubits is essential for the performance of complex calculations in quantum systems, highlighting the significance of coherence and error correction. Understanding the importance of coherence in preventing and rectifying errors in quantum computations is crucial. This paper aims to explore the critical aspects of quantum entanglement and qubit interactions, which are foundational to the operation of quantum computers. By delving into these key concepts, the paper aims to elucidate their significant roles in achieving quantum supremacy. The discussion will center on how quantum entanglement, which allows enhanced computational parallelism through qubit interconnection, and efficient qubit interactions vital for complex computations, contribute to surpassing the capabilities of classical computers. Comprehending these principles is crucial for advancing quantum computing technology and overcoming the challenges to unleash its full potential.