ConQEC: Concolic Testing for Quantum Error-Correcting Code Implementations

The gist: ConQEC presents a concolic testing framework for Quantum Error-Correcting Code (QECC) implementations by combining concrete fault replay with symbolic repairpath constraints to generate tests that expose fault–syndrome–decoder–recovery (FSDR) diagnostics.

Problem Statement

Existing QECC verification techniques prove formal obligations, but developers lack a scalable testing workflow that generates concrete faults and explains where a QECC repair path first diverges. For the fault inputs to this pipeline, we focus on Pauli faults because they are the standard discrete abstraction used by QECC decoders and because general quantum errors can be decomposed into Pauli components. This creates an implementation gap between the mathematical code and the executable QECC stack. A useful QECC bug report is not just a failed final assertion; it is a replayable repair-path witness: the concrete fault, observed syndrome, decoder decision, recovery action, oracle result, and earliest divergent stage.

ConQEC Design and Workflow

ConQEC addresses scalability and diagnostic challenges with two design ideas. First, it treats each test as a Fault–Syndrome–Decoder–Recovery (FSDR) repair path and accepts a bug only after actual/reference replay produces a staged witness. Second, ConQEC makes test generation symbolic at the repair-path level: Pauli faults are represented as symbolic variables and propagated through syndrome, detector, stabilizer, decoder, recovery, and oracle predicates. The symbolic repair-path model is defined as S = ⟨ˆf, ΦF, sc, D, R⟩. This compact representation lets ConQEC solve for targeted repair-path behaviors without enumerating the concrete fault space or carrying an amplitude-level quantum state vector.

Objectives and Candidate Generation

ConQEC uses coverage objectives to target measurement outcomes, stabilizer conditions, and transition sequences. These objectives define the search space for candidate faults through constraint queries over S. For instance, a failure-directed objective asks for a stage divergence such as Dimpl(σ) ≠ Dref(σ). The process involves an SMT query that selects an unseen fault targeting the objective. Once a SAT model is found, the concrete fault F is materialized and then validated by paired replay.

Evaluation and Results

ConQEC was evaluated on generated source-level QECC families and public QECC artifacts with up to thousands of qubits. RQ1 demonstrated that ConQEC localizes seeded QECC repair-path faults by B = 2, and all 195 by B = 4. RQ2 showed that semantic objectives improve hard repair-path coverage more effectively than strong valid-input random testing. RQ3 indicated that ConQEC scales to thousand-qubit source-level campaigns; the next scaling boundary is repeated SMT solving, while paired replay remains negligible. RQ4 confirmed that the same evidence contract can be instantiated on public QECC artifacts through detector-adapter execution and wrapper-level decoder-regression replay.

Conclusion

ConQEC credits coverage and reports bugs only after paired actual/reference replay records the relevant repair-path evidence. The remaining results show that semantic objectives improve hard repair-path coverage, paired replay is not the scale bottleneck, and the same evidence contract can be instantiated on public QECC artifacts. This paper presented ConQEC, a concolic testing framework that treats QECC execution as a replay-backed repair path. The authors conclude that ConQEC detects the seeded bug in every experimental case and reports a replay-valid, fault-localizing FSDR witness for each. This framework represents a significant advancement over prior methods by providing developer-facing debugging evidence. The ConQEC source code and experimental artifacts supporting this study are available at https://github.com/Hikari-H N/conqec-qse-artifact.

--- Page 1 ---

ConQEC: Concolic Testing for Quantum Error-Correcting Code Implementations

Zihao Li1,2,3, Ji Guan1,2, Mingsheng Ying4

Key Laboratory of System Software (Chinese Academy of Sciences), Beijing, China

Institute of Software, Chinese Academy of Sciences, Beijing, China

University of Chinese Academy of Sciences, Beijing, China

Centre for Quantum Software and Information, University of Technology Sydney, Sydney Australia

lizh@ios.ac.cn; guanj@ios.ac.cn; Mingsheng Ying@uts.edu.au

Abstract—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 repairpath 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 amplitudelevel 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 replayvalid, fault-localizing FSDR witness for each. Index Terms—quantum software testing, quantum error correction, concolic testing, symbolic execution, automated test generation, debugging, failure witnesses

I. INTRODUCTION

Quantum programs are increasingly becoming components of larger software stacks. Recent work studies coverage criteria and coverage-guided test generation [1]–[3], bug studies and bug benchmarks [4], [5], static analysis [6], runtime assertions [7]–[8], and compiler verification [9]. Together, these efforts show that quantum software increasingly raises familiar software-engineering questions: how to generate effective tests, measure meaningful coverage, and localize implementation failures under quantum-specific semantics. Quantum error-correcting code (QECC) implementations make this need especially acute. QECCs are the basic mechanism by which fault-tolerant quantum computers protect logical quantum information from noisy physical hardware [10]–[16]. Instead of storing information in a single fragile physical qubit (quantum bit), a QECC encodes it into a larger block of physical qubits, repeatedly extracts syndrome information to infer possible faults, and applies recovery operations intended to restore the logical state.

1. Scalable repair-path generation allows ConQEC to target thousand-qubit QECC behaviors by encoding Pauli faults, syndrome predicates, decoder/recovery relations, and oracle checks as symbolic constraints instead of amplitude level reasoning. This enables the framework to generate tests that expose fault–syndrome–decoder–recovery (FSDR) diagnostics without being limited by exponentially increasing state space.

2. ConQEC produces replay-backed FSDR witnesses that localize the earliest divergent stage, such as Decoder misdispatch, allowing developers to pinpoint exactly where an implementation diverges from a reference contract, rather than just reporting a final logical failure.

3. Semantic coverage objectives allow ConQEC to target hard stabilizer obligations more effectively than random testing by recording not only whether a check fired but also the number of selected fault atoms that touched that check, distinguishing between different fault weights.

4. The system can evaluate the effectiveness of repair-path semantic guidance over valid-input random testing by demonstrating superior coverage on stabilizer conditions and transition sequences across various qubit scales compared to random sampling.

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.