In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two ingenious quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor's algorithm.In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two ingenious quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor's algorithm.

arXiv:1911.12855Nov 28, 20195 citations

Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer

Gushu Li, Li Zhou, Nengkun Yu +3 more

Nov 28, 20194 citations

A Framework for the Efficient Evaluation of Runtime Assertions on Quantum Computers

Damian Rovara, Lukas Burgholzer, Robert Wille

The continuous growth of quantum computing and the increasingly complex quantum programs resulting from it lead to unprecedented obstacles in ensuring program correctness. Runtime assertions are, therefore, becoming a crucial tool in the development of quantum programs. They assist developers in the debugging process and help to test and verify the program. However, while assertions can be implemented in a straightforward manner on classical computers, physical limitations of quantum computers pose considerable challenges for the evaluation of quantum assertions. Access to the quantum state of a program is limited, execution time is expensive and noise can significantly distort measurement outcomes. To address these problems, this work proposes a framework that assists developers in the evaluation of runtime assertions on real quantum computers. It translates a variety of assertions into sets of measurements, reduces execution overhead where possible and evaluates the measurement results after the execution even in the presence of noise. This approach substantially aids developers in the debugging process, enabling efficient assertion-driven debugging even in large programs. The proposed framework is available as an open-source implementation at https://github.com/munich-quantum-toolkit/debuggerThe continuous growth of quantum computing and the increasingly complex quantum programs resulting from it lead to unprecedented obstacles in ensuring program correctness. Runtime assertions are, therefore, becoming a crucial tool in the development of quantum programs. They assist developers in the debugging process and help to test and verify the program. However, while assertions can be implemented in a straightforward manner on classical computers, physical limitations of quantum computers pose considerable challenges for the evaluation of quantum assertions. Access to the quantum state of a program is limited, execution time is expensive and noise can significantly distort measurement outcomes. To address these problems, this work proposes a framework that assists developers in the evaluation of runtime assertions on real quantum computers. It translates a variety of assertions into sets of measurements, reduces execution overhead where possible and evaluates the measurement results after the execution even in the presence of noise. This approach substantially aids developers in the debugging process, enabling efficient assertion-driven debugging even in large programs. The proposed framework is available as an open-source implementation at https://github.com/munich-quantum-toolkit/debugger

arXiv:2505.03885IEEE International Conference on Quantum Software (QSW)Jul 1, 20260 citations

Exploiting Quantum Assertions for Error Mitigation and Quantum Program Debugging

Peiyi Li, Ji Liu, Yangjia Li +1 more

An assertion is a predicate that should be evaluated true during program execution. In this paper, we present the development of quantum assertion schemes and show how they are used for hardware error mitigation and software debugging. Compared to assertions in classical programs, quantum assertions are challenging due to the no-cloning theorem and potentially destructive measurement. We discuss how these challenges can be circumvented such that certain properties of quantum states can be verified non-destructively during program execution. Furthermore, we show that besides detecting program bugs, dynamic assertion circuits can mitigate noise effects via post-selection of the assertion results. Our case studies demonstrate the use of quantum assertions in various quantum algorithms.An assertion is a predicate that should be evaluated true during program execution. In this paper, we present the development of quantum assertion schemes and show how they are used for hardware error mitigation and software debugging. Compared to assertions in classical programs, quantum assertions are challenging due to the no-cloning theorem and potentially destructive measurement. We discuss how these challenges can be circumvented such that certain properties of quantum states can be verified non-destructively during program execution. Furthermore, we show that besides detecting program bugs, dynamic assertion circuits can mitigate noise effects via post-selection of the assertion results. Our case studies demonstrate the use of quantum assertions in various quantum algorithms.

IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD)Oct 1, 20227 citations

Statistical assertions for validating patterns and finding bugs in quantum programs

Yipeng Huang, Margaret Martonosi

In support of the growing interest in quantum computing experimentation, programmers need new tools to write quantum algorithms as program code. Compared to debugging classical programs, debugging quantum programs is difficult because programmers have limited ability to probe the internal states of quantum programs; those states are difficult to interpret even when observations exist; and programmers do not yet have guidelines for what to check for when building quantum programs. In this work, we present quantum program assertions based on statistical tests on classical observations. These allow programmers to decide if a quantum program state matches its expected value in one of classical, superposition, or entangled types of states. We extend an existing quantum programming language with the ability to specify quantum assertions, which our tool then checks in a quantum program simulator. We use these assertions to debug three benchmark quantum programs in factoring, search, and chemistry. We share what types of bugs are possible, and lay out a strategy for using quantum programming patterns to place assertions and prevent bugs.In support of the growing interest in quantum computing experimentation, programmers need new tools to write quantum algorithms as program code. Compared to debugging classical programs, debugging quantum programs is difficult because programmers have limited ability to probe the internal states of quantum programs; those states are difficult to interpret even when observations exist; and programmers do not yet have guidelines for what to check for when building quantum programs. In this work, we present quantum program assertions based on statistical tests on classical observations. These allow programmers to decide if a quantum program state matches its expected value in one of classical, superposition, or entangled types of states. We extend an existing quantum programming language with the ability to specify quantum assertions, which our tool then checks in a quantum program simulator. We use these assertions to debug three benchmark quantum programs in factoring, search, and chemistry. We share what types of bugs are possible, and lay out a strategy for using quantum programming patterns to place assertions and prevent bugs.

arXiv:1905.09721Proceedings - International Symposium on Computer Architecture/ProceedingsJun 14, 2019164 citations

The Time-Space Complexity of Checking Multiple Assertions in Quantum Programs

Shengyuan Yang, Charles Yuan

Runtime assertions are a promising mechanism for testing and debugging quantum programs. But unlike the classical world, checking a quantum program that contains multiple assertions often requires using additional space or running the program additional times. For example, on current quantum hardware where mid-circuit measurement is restricted or costly, an assertion's pass/fail outcome cannot be revealed immediately. Instead, it is routed into an ancilla qubit during execution and read out by a terminal measurement. For a program with $n$ assertions, a naive strategy uses $n$ ancillas to learn all $n$ outcomes, while an alternative uses one ancilla but repeats program execution over $n$ rounds, checking one assertion per round. Both satisfy $S \cdot T = O(n)$ , where $S$ is the number of ancillas and $T$ the number of executions: a fundamental time-space trade-off. Can one do asymptotically better? We reveal that the answer depends sharply on the information to be learned. Reporting the outcomes of all assertions requires linear complexity, but two partial-information tasks of detecting whether any assertion fails, and of identifying the first failing assertion, require only logarithmic complexity -- an asymptotic improvement. Moreover, the checking strategies for these tasks can trade time for space in useful ways. In this work, we formalize the complexity of checking multiple assertions in a quantum program. Using this definition, we establish its landscape of asymptotic lower bounds and constructive upper bounds. We confirm via a case study on Grover's algorithm that the resource costs of constructed strategies match theoretical predictions, illustrating the practical design space for quantum programmers.Runtime assertions are a promising mechanism for testing and debugging quantum programs. But unlike the classical world, checking a quantum program that contains multiple assertions often requires using additional space or running the program additional times. For example, on current quantum hardware where mid-circuit measurement is restricted or costly, an assertion's pass/fail outcome cannot be revealed immediately. Instead, it is routed into an ancilla qubit during execution and read out by a terminal measurement. For a program with $n$ assertions, a naive strategy uses $n$ ancillas to learn all $n$ outcomes, while an alternative uses one ancilla but repeats program execution over $n$ rounds, checking one assertion per round. Both satisfy $S \cdot T = O(n)$, where $S$ is the number of ancillas and $T$ the number of executions: a fundamental time-space trade-off. Can one do asymptotically better? We reveal that the answer depends sharply on the information to be learned. Reporting the outcomes of all assertions requires linear complexity, but two partial-information tasks of detecting whether any assertion fails, and of identifying the first failing assertion, require only logarithmic complexity -- an asymptotic improvement. Moreover, the checking strategies for these tasks can trade time for space in useful ways. In this work, we formalize the complexity of checking multiple assertions in a quantum program. Using this definition, we establish its landscape of asymptotic lower bounds and constructive upper bounds. We confirm via a case study on Grover's algorithm that the resource costs of constructed strategies match theoretical predictions, illustrating the practical design space for quantum programmers.

cs.PLCross-listedarXiv:2607.11665Jul 14, 20260 citations

n

assertions, a naive strategy uses

n

ancillas to learn all

n

outcomes, while an alternative uses one ancilla but repeats program execution over

n

rounds, checking one assertion per round. Both satisfy

S \cdot T = O(n)

, where

S

is the number of ancillas and

T

the number of executions: a fundamental time-space trade-off. Can one do asymptotically better? We reveal that the answer depends sharply on the information to be learned. Reporting the outcomes of all assertions requires linear complexity, but two partial-information tasks of detecting whether any assertion fails, and of identifying the first failing assertion, require only logarithmic complexity -- an asymptotic improvement. Moreover, the checking strategies for these tasks can trade time for space in useful ways. In this work, we formalize the complexity of checking multiple assertions in a quantum program. Using this definition, we establish its landscape of asymptotic lower bounds and constructive upper bounds. We confirm via a case study on Grover's algorithm that the resource costs of constructed strategies match theoretical predictions, illustrating the practical design space for quantum programmers.