Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over H,X,C-NOT: CSS Constructions, Soundness, and Mutation-Based Validation

arXiv:2610.03794 · quant-ph, cs.ET, cs.LO · Submitted 2026-10-01 · Read on arXiv

quant-ph, cs.ET, cs.LO

Submitted: 2026-10-01

Updated: 2026-10-01

Comments: Accepted for publication in SN Computer Science, final version will be available through journal once published. Abstract is modified to account for arXiv character count

DOI: 10.1007/s42979-026-05395-6

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Abstraction — 1× in this paper · explained in 1 episode
• Entanglement — 1× in this paper · explained in 4 episodes
• Formal Verification — 1× in this paper · explained in 2 episodes
• Verification — 1× in this paper · explained in 2 episodes

Sources

• Going Beyond Bell's Theorem
• The Heisenberg Representation of Quantum Computers

Related papers

• Reconquering Bell sampling on qudits: stabilizer learning and testing, quantum pseudorandomness bounds, and more
• Encrypted clones can leak: Classification of informative subsets in Quantum Encrypted Cloning
• Polynomial-time classical and quantum simulation of quantum impurity models
• Incoherent Imaging with Spatially Structured Quantum Probes
• A quasiparticle-protected superconducting qubit
• Theory of quantum-enhanced interferometry with general Markovian light sources