Pith. sign in

REVIEW 4 minor 59 references

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

T0 review · 0 major / 4 minor · reviewed 2026-07-14 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Checking whether any assertion fails, or which fails first, needs only logarithmic ancillas and rounds in quantum programs; listing every failure needs linear cost.

desk verdict Tight asymptotic landscape for multi-assertion checking: ListAll is linear, ExistFail/FirstFail are logarithmic, with matching constructions and a clean transfer to mid-circuit S+M. read the letter →

arxiv 2607.11665 v1 pith:HLTISC3I submitted 2026-07-13 cs.PL quant-ph

Shengyuan Yang , Charles Yuan This is my paper · ORCID
classification cs.PLquant-ph
keywords quantumruntimeassertionstime-spacetrade-offterminalmeasurementExistFailFirstListAllunitarytransitionsystemsprogramtesting
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Quantum programs cannot check many runtime assertions the way classical programs do: mid-circuit measurement is often costly or restricted, so each assertion's pass/fail outcome must be routed into helper (ancilla) qubits and read out only at the end. For n assertions the obvious strategies either use n ancillas in one run or one ancilla across n runs, both linear in n. This paper proves the cost is not always linear. Full reporting of every failure outcome really does require a product of ancillas and runs that is linear in n. But merely detecting whether any assertion fails, or identifying the index of the earliest failure, can be done with only logarithmic resources, and the strategies can trade runs against ancillas. The results rest on a formal model of checking strategies that never rewrite the program or inspect its predicates, only route outcomes through declared checkers into ancillas. Matching lower bounds come from reducing the problem to distinguishing bit-string patterns with unitary transition systems whose dimension is forced by reversibility. A Grover case study shows the predicted space savings appear in concrete circuits.

What carries the argument

The unitary-transition-system reduction: every legal checking strategy induces a multi-round unitary transition system that must distinguish the corresponding bit-string pattern (Exist, First, or List). Dimension lower bounds on those systems transfer directly into ancilla lower bounds; the matching constructions realize reversible counters and index-register transpositions that never need linear history.

What would settle it

Exhibit a uniform terminal-measurement strategy that solves ExistFail or FirstFail on arbitrary programs with o(log n) ancillas in one round, or that solves ListAll with S·T = o(n); or show that a concrete family of programs admits a cheaper strategy once the separation between program and checkers is relaxed.

Watch

Extended reading notes

Core claim

Under terminal measurement only, the three natural assertion-checking tasks have sharply different asymptotic complexity: ListAll requires S·T = Θ(n), while ExistFail and FirstFail admit single-round S = Θ(log n) and, in the disjoint multi-round setting, S = Θ(log(1 + n/T)). When rounds may overlap, ExistFail further reaches S = Θ((log n)/T) for T up to O(log n / log log n); FirstFail does not improve beyond the disjoint trade-off. Matching constructive strategies (modulo counters, index transpositions, LCM fingerprinting) and lower bounds are given for every regime.

Load-bearing premise

Strategies may only move information out of the program through the declared assertion checkers into ancillas; they cannot look at the program text, rewrite it, or exploit correlations with the final output.

Editorial extensions

If this is right

  • On hardware where mid-circuit measurement is expensive, programmers can replace n measurements or n ancillas by O(log n) resources when only existence or first-failure information is needed.
  • Every single-round ancilla lower bound also lower-bounds the sum of ancillas plus measurements in the mid-circuit model, giving immediate resource bounds for projection-based assertion schemes.
  • Disjoint multi-round strategies supply concrete ways to trade extra ancillas for fewer mid-circuit measurements while preserving correctness.
  • The same reversible-counter and index-transposition primitives can be reused as building blocks for other multi-assertion coordination tasks.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Adaptive round selection (binary-search style) is unlikely to improve the leading asymptotics in the terminal model, but may cut constant factors or gate overhead once mid-circuit feed-forward is free.
  • The same information-extraction view under limited measurement may apply to syndrome aggregation in quantum error correction and to multi-point checks in circuit verification.
  • Once mid-circuit measurement becomes cheap, the interesting open question shifts from total S+M to the separate trade-off between S and M.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

0 major / 4 minor

Summary. The paper formalizes the time–space complexity of coordinating multiple runtime assertions in quantum programs under the terminal-measurement model. It defines three tasks (ListAll, ExistFail, FirstFail) and proves a landscape of matching asymptotic bounds (Table 1): ListAll requires S·T=Θ(n), while ExistFail and FirstFail admit single-round S=Θ(log n) and disjoint multi-round S=Θ(log(1+n/T)); general multi-round ExistFail further reaches S=Θ((log n)/T) for T=O(log n/log log n). Upper bounds are given by explicit constructive strategies (modulo increment, index transposition, LCM fingerprinting, partitioned reporting) with concrete gate/measurement costs; lower bounds transfer via a unitary-transition-system reduction and orthogonality/packing arguments. A Qiskit case study on Grover’s algorithm confirms that concrete resource costs track the asymptotics.

Significance. If the results hold, the work supplies the first rigorous complexity landscape for multi-assertion checking in quantum programs, a cost orthogonal to individual predicate circuits. The logarithmic strategies for ExistFail and FirstFail, together with the explicit time–space trade-offs, give programmers concrete design points on hardware where mid-circuit measurement is costly. The constructions are uniform, reversible, and accompanied by full proofs and a reproducible Qiskit implementation; the mid-circuit transfer theorems further future-proof the bounds. The contrast with classical intuition (ExistFail harder, FirstFail easier under reversibility) is a genuine conceptual contribution to quantum program analysis.

minor comments (4)
  1. [Table 1] Table 1 and the surrounding text state the general multi-round ExistFail bound only for T=O(log n/log log n); a brief forward pointer in the table caption to the open regime discussed after Theorem 5.15 would help readers who stop at the summary table.
  2. [Section 3.4] The contiguity assumption required for the mid-circuit upper-bound transfer (Theorem 3.11) is mild and holds for all presented strategies, but a one-sentence reminder when the theorem is invoked in Section 3.4 would make the hypothesis fully local.
  3. [Table 3] In the Grover case study the percentages are relative to the single-round ListAll baseline; adding the absolute qubit and gate counts of the bare (uninstrumented) program in a footnote or table note would make the amortization claim easier to verify at a glance.
  4. A few minor typographical inconsistencies appear (e.g., “time–space” versus “time-space”, occasional missing thin spaces around ·). A final copy-edit pass would polish the presentation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: asymptotic bounds and constructions are self-contained against the paper's own model definitions.

full rationale

The paper's central claims (Table 1 landscape of S·T bounds for ListAll/ExistFail/FirstFail) are derived from first-principles definitions of strategies (Defs. 3.3–3.6), the unitary-transition-system reduction (Lems. 4.3–4.4), and explicit constructions (Strategies 5.4, 5.9, 5.13, 6.3, 6.9, 7.3) whose costs are calculated directly from gate counts and register sizes. Lower bounds (Thms. 5.1, 5.7, 5.11, 6.1, 6.7, 6.11, 7.1) follow from orthogonality/packing arguments on those same objects and do not import fitted parameters or uniqueness theorems. The NUOBDD citation [22] is background agreement only; Lemma 5.2 is proved independently. The Grover case study reports end-to-end resource counts relative to the paper's own ListAll baseline and confirms consistency with the asymptotics, without circular prediction. No step reduces a claimed result to its own input by construction.

Assumptions & free parameters 0 free parameters · 5 assumptions · 1 invented entities

The work is asymptotic complexity theory over a standard quantum circuit model. Load-bearing ingredients are modeling choices (terminal measurement, checker-unitary interface, uniform strategies) and standard unitary/measurement math—not fitted constants or new physical entities. The unitary transition system is a proof device, not an ontological postulate.

assumptions (5)
  • standard math Quantum evolution is unitary between measurements; computational-basis measurement collapses amplitudes to classical outcomes (standard model).
    Background throughout Sec. 2 and all strategy semantics.
  • domain assumption Assertion checking is modeled by checker unitaries C_i = P_i⊗I + (I−P_i)⊗X that route pass/fail into an ancilla without mid-circuit measurement of the program (Eq. 1).
    Abstraction of prior non-destructive assertion schemes; all strategies and bounds are stated relative to this interface (Sec. 3.1).
  • domain assumption Strategies are uniform and may only enable declared assertions and process ancillas; they do not inspect program text, predicates, or exploit program-output correlations (Defs. 3.3–3.4).
    Enforces the testing contract and enables the transfer to bit-string distinguishing tasks (Lem. 4.4).
  • domain assumption Gap promise: each assertion failure probability is either 0 or at least η>0 (Sec. 3.5).
    Used for probabilistic task semantics and semantic-stability theorems; deterministic lower bounds are the special case p_i∈{0,1}.
  • ad hoc to paper For mid-circuit upper-bound transfer, enabled assertion sets per round are contiguous in index order (Thm. 3.11).
    Mild structural condition stated for all strategies in the paper; needed to concatenate segments with measure-and-reset.
invented entities (1)
  • Finite-dimensional unitary transition system (Def. 4.1) independent evidence
    purpose: Proof device that reduces assertion-checking lower bounds to bit-string pattern distinguishing under unitary updates and terminal measurement.
    Mathematical abstraction analogous to branching programs/NUOBDDs; not a physical postulate. Independent mathematical content, but no external empirical handle required.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Time-Space Complexity of Checking Multiple Assertions in Quantum Programs." pith.science (2026). https://pith.science/paper/HLTISC3I

@misc{pith2026260711665,
  author       = {Pith},
  title        = {Pith review of: The Time-Space Complexity of Checking Multiple Assertions in Quantum Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/HLTISC3I}},
  note         = {Machine review of arXiv:2607.11665}
}
abstract

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.

Figures

Figures reproduced from arXiv: 2607.11665 by the authors.

Figure 1
Figure 1. A quantum program with three assertions. Both qubits x and y are initialized to zero. Running Example. To illustrate checking of multiple assertions in this terminal-measurement model, we present the program in [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. The logical-OR based assertion circuit construction (a) can be transformed by applying an additional [PITH_FULL_IMAGE:figures/full_fig_p031_3.png] view at source ↗
Figure 4
Figure 4. The NDD-based assertion circuit, which already aligns with the checker unitary. [PITH_FULL_IMAGE:figures/full_fig_p031_4.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

59 extracted references · 15 canonical work pages

  1. [1]

    Parosh Aziz Abdulla, Yo-Ga Chen, Yu-Fang Chen, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Fang-Yi Lo, and Wei-Lun Tsai. 2025. Verifying Quantum Circuits with Level-Synchronized Tree Automata.Proc. ACM Program. Lang.9, POPL, Article 32 (Jan. 2025), 31 pages. doi:10.1145/3704868

    doi:10.1145/3704868 2025

  2. [2]

    Farid Ablayev, Aida Gainutdinova, Marek Karpinski, Cristopher Moore, and Christopher Pollett. 2005. On the computational power of probabilistic and quantum branching program.Information and Computation203, 2 (2005), 145–162. doi:10.1016/j.ic.2005.04.003

    work page doi:10.1016/j.ic.2005.04.003 2005

  3. [3]

    Shaukat Ali, Paolo Arcaini, Xinyi Wang, and Tao Yue. 2021. Assessing the Effectiveness of Input and Output Coverage Criteria for Testing Quantum Programs. InIEEE Conference on Software Testing, Verification and Validation. 13–23. doi:10.1109/ICST49551.2021.00014

    doi:10.1109/icst49551.2021.00014 2021

  4. [4]

    Jatin Arora, Mingkuan Xu, Sam Westrick, Pengyu Liu, Dantong Li, Yongshan Ding, and Umut A. Acar. 2025. Local Optimization of Quantum Circuits. In2025 IEEE International Conference on Quantum Computing and Engineering (QCE), Vol. 01. 572–583. doi:10.1109/QCE65121.2025.00069

    doi:10.1109/qce65121.2025.00069 2025

  5. [5]

    Martin Avanzini, Georg Moser, Romain Péchoux, and Simon Perdrix. 2024. On the Hardness of Analyzing Quantum Programs Quantitatively. InEuropean Symposium on Programming. 31–58. doi:10.1007/978-3-031-57267-8_2

    doi:10.1007/978-3-031-57267-8_2 2024

  6. [6]

    Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, and Li Zhou. 2019. Relational proofs for quantum programs. Proc. ACM Program. Lang.4, POPL, Article 21 (Dec. 2019), 29 pages. doi:10.1145/3371089

    work page doi:10.1145/3371089 2019

  7. [7]

    Thinniyam, and Georg Zetzsche

    Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. 2022. Context-bounded verification of thread pools.Proc. ACM Program. Lang.6, POPL, Article 17 (Jan. 2022), 28 pages. doi:10.1145/3498678

    work page doi:10.1145/3498678 2022

  8. [8]

    Charles H. Bennett. 1989. Time/Space Trade-Offs for Reversible Computation.SIAM J. Comput.18, 4 (1989), 766–776. doi:10.1137/0218053

    doi:10.1137/0218053 1989

Show all 59 references
  1. [9]

    Evered, Alexandra A

    Dolev Bluvstein, Simon J. Evered, Alexandra A. Geim, Sophie H. Li, Hengyun Zhou, Tom Manovitz, Sepehr Ebadi, Madelyn Cain, Marcin Kalinowski, Dominik Hangleiter, J. Pablo Bonilla Ataides, Nishad Maskara, Iris Cong, Xun Gao, Pedro Sales Rodriguez, Thomas Karolyshyn, Giulia Seme...

    2023 doi

  2. [10]

    Borodin and S

    A. Borodin and S. Cook. 1982. A Time-Space Tradeoff for Sorting on a General Sequential Model of Computation. SIAM J. Comput.11, 2 (1982), 287–297. doi:10.1137/0211022

    1982 doi

  3. [11]

    Costin Bădescu, Ryan O’Donnell, and John Wright. 2019. Quantum state certification. InACM SIGACT Symposium on Theory of Computing. 503–514. doi:10.1145/3313276.3316344

    2019 doi

  4. [12]

    Jacques Carette, Chris Heunen, Robin Kaarsgaard, and Amr Sabry. 2024. With a Few Square Roots, Quantum Computing Is as Easy as Pi.Proc. ACM Program. Lang.8, POPL, Article 19 (Jan. 2024), 29 pages. doi:10.1145/3632861

    2024 doi

  5. [13]

    Yanbin Chen, Innocenzo Fulginiti, and Christian B. Mendl. 2024. Reducing Mid-Circuit Measurements via Probabilistic Circuits. InIEEE International Conference on Quantum Computing and Engineering. 952–958. doi:10.1109/QCE60285. 2024.00114

    2024 doi

  6. [14]

    Yanbin Chen, Innocenzo Fulginiti, and Christian B. Mendl. 2025. Optimization Framework for Reducing Mid-circuit Measurements and Resets. InInternational Conference on Computational Science Workshops. 150–164. doi:10.1007/978- 3-031-97570-7_13

    2025 doi

  7. [15]

    Andrea Colledan and Ugo Dal Lago. 2025. Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages.Proc. ACM Program. Lang.9, POPL, Article 47 (Jan. 2025), 31 pages. doi:10.1145/3704883

    2025 doi

  8. [16]

    A. D. Córcoles, Maika Takita, Ken Inoue, Scott Lekuch, Zlatko K. Minev, Jerry M. Chow, and Jay M. Gambetta. 2021. Exploiting Dynamic Quantum Circuits in a Quantum Algorithm with Superconducting Qubits.Physical Review Letters 127, 10 (2021), 100501. doi:10.1103/PhysRevLett.127.100501

    2021 doi

  9. [17]

    Madhusudan

    Azadeh Farzan and P. Madhusudan. 2009. The Complexity of Predicting Atomicity Violations. InProceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Pract...

    2009 doi

  10. [19]

    Daniel Fortunato, José Campos, and Rui Abreu. 2022. QMutPy: a mutation testing tool for Quantum algorithms and applications in Qiskit. InACM SIGSOFT International Symposium on Software Testing and Analysis. 797–800. doi:10.1145/3533767.3543296

    2022 doi

  11. [20]

    Daniel Fortunato, José Campos, and Rui Abreu. 2024. Gate Branch Coverage: A Metric for Quantum Software Testing. InACM International Workshop on Quantum Software Engineering. 15–18. doi:10.1145/3663531.3664753

    2024 doi

  12. [21]

    J. P. Gaebler, C. H. Baldwin, S. A. Moses, J. M. Dreiling, C. Figgatt, M. Foss-Feig, D. Hayes, and J. M. Pino. 2021. Suppression of midcircuit measurement crosstalk errors with micromotion.Physical Review A104, 6 (2021), 062440. The Time–Space Complexity of Checking Multiple A...

    2021 doi

  13. [22]

    Aida Gainutdinova and Abuzer Yakaryılmaz. 2017. Nondeterministic Unitary OBDDs. InInternational Computer Science Symposium in Russia. 126–140. doi:10.1007/978-3-319-58747-9_13

    2017 doi

  14. [23]

    Jingliang Gao. 2015. Quantum union bounds for sequential projective measurements.Phys. Rev. A92, 5 (Nov 2015), 052331. doi:10.1103/PhysRevA.92.052331

    2015 doi

  15. [24]

    Gay and Rajagopal Nagarajan

    Simon J. Gay and Rajagopal Nagarajan. 2005. Communicating quantum processes.SIGPLAN Not.40, 1 (Jan. 2005), 145–157. doi:10.1145/1047659.1040318

    2005 doi

  16. [25]

    György P Gehér, Marcin Jastrzebski, Earl T Campbell, and Ophelia Crawford. 2025. To reset, or not to reset—that is the question.npj Quantum Information11 (2025), 39. doi:10.1038/s41534-025-00998-y

    2025 doi

  17. [26]

    Goharshady, Kerim Kochekov, Tian Shu, and Ahmed Khaled Zaher

    Amir K. Goharshady, Kerim Kochekov, Tian Shu, and Ahmed Khaled Zaher. 2026. Parameterized Algorithms and Complexity for Function Merging with Branch Reordering.Proc. ACM Program. Lang.10, PLDI, Article 204 (June 2026), 23 pages. doi:10.1145/3808282

    2026 doi

  18. [27]

    Google Quantum AI. 2025. Quantum error correction below the surface code threshold.Nature638 (2025), 920–926. doi:10.1038/s41586-024-08449-y

    2025 doi

  19. [28]

    Lov K. Grover. 1996. A fast quantum mechanical algorithm for database search. InACM Symposium on Theory of Computing. 212–219. doi:10.1145/237814.237866

    1996 doi

  20. [29]

    Wallman, and Irfan Siddiqi

    Akel Hashim, Arnaud Carignan-Dugas, Larry Chen, Christian Jünger, Neelay Fruitwala, Yilun Xu, Gang Huang, Joel J. Wallman, and Irfan Siddiqi. 2025. Quasiprobabilistic Readout Correction of Midcircuit Measurements for Adaptive Feedback via Measurement Randomized Compiling.PRX Q...

    2025 doi

  21. [30]

    Shahin Honarvar, Mohammad Reza Mousavi, and Rajagopal Nagarajan. 2020. Property-based Testing of Quantum Programs in Q#. InIEEE/ACM International Conference on Software Engineering Workshops. 430–435. doi:10.1145/ 3387940.3391459

    2020

  22. [31]

    Daniel Hothem, Jordan Hines, Charles Baldwin, Dan Gresh, Robin Blume-Kohout, and Timothy Proctor. 2025. Measur- ing error rates of mid-circuit measurements.Nature Communications16 (2025), 5761. doi:10.1038/s41467-025-60923-x

    2025 doi

  23. [32]

    Yipeng Huang and Margaret Martonosi. 2019. Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs. InInternational Symposium on Computer Architecture. 541–553. doi:10.1145/3307650.3322213

    2019 doi

  24. [33]

    IBM Quantum. 2022. Bringing the full power of dynamic circuits to Qiskit Runtime. https://www.ibm.com/quantum/ blog/quantum-dynamic-circuits

    2022

  25. [34]

    IBM Quantum. 2025. Classical feedforward and control flow. https://quantum.cloud.ibm.com/docs/en/guides/classical- feedforward-and-control-flow

    2025

  26. [35]

    IBM Quantum. 2025. Utility-scale dynamic circuits now available for all users. https://www.ibm.com/quantum/blog/ utility-scale-dynamic-circuits

    2025

  27. [36]

    Chan Gu Kang, Joonghoon Lee, and Hakjoo Oh. 2024. Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification. InACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. 140–164. doi:10.1145/3689716

    2024 doi

  28. [37]

    Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie. 2020. Projection-based Runtime Assertions for Testing and Debugging Quantum Programs. InACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications. 1–29. doi:10.1145/3428218

    2020 doi

  29. [38]

    Byrd, and Huiyang Zhou

    Ji Liu, Gregory T. Byrd, and Huiyang Zhou. 2020. Quantum Circuits for Dynamic Runtime Assertions in Quantum Computation. InACM International Conference on Architectural Support for Programming Languages and Operating Systems. 1017–1030. doi:10.1145/3373376.3378488

    2020 doi

  30. [39]

    Ji Liu and Huiyang Zhou. 2021. Systematic Approaches for Precise and Approximate Quantum State Runtime Assertion. InIEEE International Symposium on High-Performance Computer Architecture. 179–193. doi:10.1109/HPCA51647.2021. 00025

    2021 doi

  31. [40]

    Peixun Long and Jianjun Zhao. 2024. Testing Multi-Subroutine Quantum Programs: From Unit Testing to Integration Testing.ACM Transactions on Software Engineering and Methodology33, 6 (2024). doi:10.1145/3656339

    2024 doi

  32. [41]

    Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka, and Emanuele D’Osualdo. 2026. RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing.Proc. ACM Program. Lang.10, POPL, Article 6 (Jan. 2026), 30 pages. doi:10.1145/3776648

    2026 doi

  33. [42]

    Eñaut Mendiluze, Shaukat Ali, Paolo Arcaini, and Tao Yue. 2022. Muskit: a mutation analysis tool for quantum software testing. InIEEE/ACM International Conference on Automated Software Engineering. 1266–1270. doi:10.1109/ASE51524. 2021.9678563

    2022 doi

  34. [43]

    Ashley Montanaro and Ronald de Wolf. 2013. A Survey of Quantum Property Testing.Theory of Computing7 (2013), 1–81. doi:10.4086/toc.gs.2016.007

    2013 doi

  35. [44]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2011.Quantum Computation and Quantum Information(10th ed.). doi:10. 1017/CBO9780511976667 28 Yang and Yuan

    2011

  36. [45]

    Damian Rovara, Lukas Burgholzer, and Robert Wille. 2025. Automatically Refining Assertions for Efficient Debugging of Quantum Programs. InIEEE International Conference on Quantum Computing and Engineering. 766–772. doi:10. 1109/QCE65121.2025.00088

    2025

  37. [46]

    Damian Rovara, Lukas Burgholzer, and Robert Wille. 2025. A framework for the efficient evaluation of runtime assertions on quantum computers. arXiv:2505.03885 [quant-ph] doi:10.48550/arXiv.2505.03885

    2025 doi arXiv

  38. [47]

    Martin Sauerhoff and Detlef Sieling. 2005. Quantum branching programs and space-bounded nonuniform quantum complexity.Theoretical Computer Science334, 1 (2005), 177–225. doi:10.1016/j.tcs.2004.12.031

    2005 doi

  39. [48]

    Zheng Shi, Lasse Møldrup, Umang Mathur, and Andreas Pavlogiannis. 2026. The Complexity of Testing Message- Passing Concurrency.Proc. ACM Program. Lang.10, POPL, Article 1 (Jan. 2026), 32 pages. doi:10.1145/3776643

    2026 doi

  40. [49]

    Cross, Frederic T

    Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, and Ronghui Gu. 2022. Giallar: push-button verification for the Qiskit Quantum compiler. InProceedings of the 43rd ACM SIGPLAN International Conference on Programming Languag...

    2022 doi

  41. [50]

    Hünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur, and Andreas Pavlogiannis. 2023. Optimal Reads-From Consistency Checking for C11-Style Memory Models.Proc. ACM Program. Lang.7, PLDI, Article 137 (June 2023), 25 pages. doi:10.1145/3591251

    2023 doi

  42. [51]

    Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. 2023. Qunity: A Unified Language for Quantum and Classical Computing.Proc. ACM Program. Lang.7, POPL, Article 32 (Jan. 2023), 31 pages. doi:10.1145/3571225

    2023 doi

  43. [52]

    Jiyuan Wang, Fucheng Ma, and Yu Jiang. 2021. Poster: Fuzz Testing of Quantum Program. InIEEE Conference on Software Testing, Verification and Validation. 466–469. doi:10.1109/ICST49551.2021.00061

    2021 doi

  44. [53]

    Xinyi Wang, Paolo Arcaini, Tao Yue, and Shaukat Ali. 2021. Application of Combinatorial Testing to Quantum Programs. InIEEE International Conference on Software Quality, Reliability and Security. 179–188. doi:10.1109/QRS54544.2021.00029

    2021 doi

  45. [54]

    Xinyi Wang, Paolo Arcaini, Tao Yue, and Shaukat Ali. 2022. QuSBT: search-based testing of quantum programs. In ACM/IEEE International Conference on Software Engineering: Companion Proceedings. 173–177. doi:10.1145/3510454. 3516839

    2022 doi

  46. [55]

    2000.Branching Programs and Binary Decision Diagrams

    Ingo Wegener. 2000.Branching Programs and Binary Decision Diagrams. Society for Industrial and Applied Mathematics. doi:10.1137/1.9780898719789

    2000 doi

  47. [56]

    Mingsheng Ying. 2012. Floyd–Hoare logic for quantum programs.ACM Trans. Program. Lang. Syst.33, 6, Article 19 (Jan. 2012), 49 pages. doi:10.1145/2049706.2049708

    2012 doi

  48. [57]

    Andreas Zeller and Ralf Hildebrandt. 2002. Simplifying and Isolating Failure-Inducing Input.IEEE Trans. Softw. Eng. 28, 2 (2002), 183–200. doi:10.1109/32.988498

    2002 doi

  49. [58]

    Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. 2023. CoqQ: Foundational Verification of Quantum Programs.Proc. ACM Program. Lang.7, POPL, Article 29 (Jan. 2023), 33 pages. doi:10.1145/3571222 The Time–Space Complexity of Checking Multiple Assertions ...

    2023 doi

  50. [59]

    Taking logarithms yields 𝑛≤ 2 log(1 + √

    2Í𝑇 𝑡=1 𝑑2 𝑡 . Taking logarithms yields 𝑛≤ 2 log(1 + √

  51. [60]

    ·Í𝑇 𝑡=1 𝑑 2 𝑡 , which rearranges to the claimed bound. □

Pith tools

Reviewed July 14, 2026 · model on record in the stance chip above.