← Back ◌ Quantum Computing —

Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement

arXiv Quantum Archived Mar 17, 2026 ✓ Full text saved

arXiv:2603.13554v1 Announce Type: new Abstract: We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure

Full text archived locally

✦ AI Summary · Claude Sonnet

Quantum Physics [Submitted on 13 Mar 2026] Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement Arun Govindankutty We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits. The method scales efficiently, verifying QPE circuits with up to 6 precision qubits and 1,024 phase qubits using under 3.5 GB of memory. Comments: The paper is accepted as a full research paper at IEEE-DCAS 2026 and final version will be available via IEEE-Xplore after the conference Subjects: Quantum Physics (quant-ph); Emerging Technologies (cs.ET); Logic in Computer Science (cs.LO) Cite as: arXiv:2603.13554 [quant-ph] (or arXiv:2603.13554v1 [quant-ph] for this version) https://doi.org/10.48550/arXiv.2603.13554 Focus to learn more Submission history From: Arun Govindankutty [view email] [v1] Fri, 13 Mar 2026 19:45:57 UTC (211 KB) Access Paper: HTML (experimental) view license Current browse context: quant-ph < prev | next > new | recent | 2026-03 Change to browse by: cs cs.ET cs.LO References & Citations INSPIRE HEP NASA ADS Google Scholar Semantic Scholar Export BibTeX Citation Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Demos Related Papers About arXivLabs Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?)

💬 Team Notes