This paper presents the first concolic testing framework explicitly designed for quantum programs. The framework introduces quantum constraint generation methods for quantum control statements that quantify quantum states and offers a symbolization method for quantum variables. Based on this framework, we generate path constraints for each concrete execution path of a quantum program. These constraints guide the exploration of new paths, with a quantum constraint solver determining outcomes to create novel input samples, thereby enhancing branch coverage. Our framework has been implemented in Python and integrated with Qiskit for practical evaluation. Experimental results show that our concolic testing framework improves branch coverage, generates high-quality quantum input samples, and detects bugs, demonstrating its effectiveness and efficiency in quantum programming and bug detection. Regarding branch coverage, our framework achieves more than 74.27% on quantum programs with under 5 qubits.
This paper presents the first concolic testing framework explicitly designed for quantum programs. The framework introduces quantum constraint generation methods for quantum control statements that quantify quantum states and offers a symbolization method for quantum variables. Based on this framework, we generate path constraints for each concrete execution path of a quantum program. These constraints guide the exploration of new paths, with a quantum constraint solver determining outcomes to create novel input samples, thereby enhancing branch coverage. Our framework has been implemented in Python and integrated with Qiskit for practical evaluation. Experimental results show that our concolic testing framework improves branch coverage, generates high-quality quantum input samples, and detects bugs, demonstrating its effectiveness and efficiency in quantum programming and bug detection. Regarding branch coverage, our framework achieves more than 74.27% on quantum programs with under 5 qubits.
Quantum error-correcting code (QECC) implementations are hybrid software-control systems: measured syndromes drive decoder dispatch, recovery actions, and logical checks. Existing QECC verification techniques can prove formal obligations, and general quantum testing can expose final failures, but developers still lack a scalable testing workflow that generates concrete faults and explains where a QECC repair path first diverges. This paper presents ConQEC, to our knowledge the first concolic testing framework for QECC implementations. By combining concrete (Pauli) fault replay with symbolic repair-path constraints, ConQEC generates tests that expose not only final logical failures but also fault--syndrome--decoder--recovery (FSDR) diagnostics: the injected fault, observed syndrome, decoder decision, recovery action, oracle result, and earliest divergent stage. Its symbolic encoding of Pauli faults, syndrome predicates, decoder and recovery relations, and oracle checks enables this diagnostic workflow to scale beyond exponentially increasing amplitude-level quantum-state reasoning. We implemented ConQEC and evaluated it on generated source-level QECC families and public QECC artifacts with up to thousands of qubits. ConQEC detects the seeded bug in every experimental case and reports a replay-valid, fault-localizing FSDR witness for each.
Quantum circuit transpilation is central to the execution of programs on noisy intermediate-scale quantum (NISQ) devices, yet it introduces reliability risks due to heuristic optimizations, parameter thresholds, and layout heuristics. Small perturbations at these decision points can silently alter program semantics, undermine optimization effectiveness, or increase hardware error susceptibility. In this work, we present a concolic testing framework for quantum compilers that systematically uncovers such vulnerabilities by combining concrete execution with symbolic reasoning. We identify and recover decision points in gate-level, parameter-sensitive, and circuit-level transpiler passes, and construct symbolic guards to drive targeted perturbations near boundary conditions. Our evaluation on representative QASMBench circuits demonstrates complete decision-point and boundary coverage of 100%, and high outcome coverage of 78%, uncovering both missed optimizations and semantic deviations in widely used Qiskit passes. These results establish that concolic testing can be applied as a practical methodology for systematically evaluating compiler robustness in the NISQ era.
Property-based testing has been previously proposed for quantum programs in Q# with QSharpCheck; however, this implementation was limited in functionality, lacked extensibility, and was evaluated on a narrow range of programs using a single property. To address these limitations, we propose QuCheck, an improved property-based testing framework for Qiskit. By leveraging Qiskit and the broader Python ecosystem, QuCheck facilitates property construction, introduces flexible input generators and assertions, and supports expressive preconditions. We assessed its effectiveness through mutation analysis on five quantum programs (2-10 qubits), varying the number of properties, inputs, and measurement shots to assess their impact on fault detection and demonstrate the effectiveness of property-based testing across a range of conditions. Results show a strong positive correlation between the mutation score (a measure of fault detection) and number of properties evaluated, with a moderate negative correlation between the false positive rate and number of measurement shots. The most thorough test configurations achieved a mean mutation score of 0.90 averaged across all five algorithms, with a false positive rate between 0 and 0.06. QuCheck identified 47.8% more faults than QSharpCheck, with execution time reduced by 67.4%. These findings highlight the viability of property-based testing for verifying quantum systems.
Quantum programs are designed to run on quantum computers, leveraging quantum circuits to solve problems that are intractable for classical machines. As quantum computing advances, ensuring the reliability of quantum programs has become increasingly important. This paper introduces NovaQ, a diversity-guided testing framework for quantum programs. NovaQ combines a distribution-based test case generator with a novelty-driven evaluation module. The generator produces diverse quantum state inputs by mutating circuit parameters, while the evaluator quantifies behavioral novelty based on internal circuit state metrics, including magnitude, phase, and entanglement. By selecting inputs that map to infrequently covered regions in the metric space, NovaQ effectively explores under-tested program behaviors. We evaluate NovaQ on quantum programs of varying sizes and complexities. Experimental results show that NovaQ consistently achieves higher test input diversity and detects more bugs than existing baseline approaches.
Errors in quantum programs are challenging to track down due to the uncertainty of quantum programs. Testing is, therefore, an indispensable method for assuring the quality of quantum software. Existing testing methods focus only on testing quantum programs with quantum circuits or single subroutines and, therefore, cannot effectively test quantum programs with multi-subroutines. In this paper, we first discuss several critical issues that must be considered when testing multi-subroutine quantum programs and point out the limitations and problems with existing testing methods. We then present a novel framework for testing multi-subroutine quantum programs that allow for both unit and integration testing. Our framework includes two novel test coverage criteria for the equivalent class partition of quantum variables to guide our testing tasks and techniques to test quantum programs with several common patterns. We also discuss how to generate test cases based on our framework. To evaluate the effectiveness of our testing framework, we implemented a tool called QSharpTester for testing Q\# programs with multiple subroutines. We used it to conduct experiments on hundreds of mutation programs deriving from seven original Q\# programs. The experimental results show that our testing methods can deal with broader types of quantum programs than existing ones and perform well on almost all faulty mutation programs.
With the growing interest in quantum programs, ensuring their correctness is a fundamental challenge. Although constraint-solving techniques can overcome some limitations of traditional testing and verification, they have not yet been sufficiently explored in the context of quantum programs. To address this gap, we present QSolver, the first quantum constraint solver. QSolver provides a structured framework for handling five types of quantum constraints and incorporates an automated assertion generation module to verify quantum states. QSolver transforms quantum programs and multi-moment constraints into symbolic representations, and utilizes an SMT solver to obtain quantum states that satisfy these constraints. To validate the correctness of the generated input states, QSolver automatically generates assertion programs corresponding to each constraint. Experimental results show that QSolver efficiently processes commonly used quantum gates and demonstrates good scalability across quantum programs of different sizes.