2021/11/26 by Anbang Wu, Gushu Li, Wu, Anbang +9 · 1 citation
Computer Science · Engineering · #FOS: Computer and information sciences #FOS: Physical sciences #Programming Languages (cs.PL) #Quantum Computing Algorithms and Architecture #Quantum Information and Cryptography #Quantum Physics (quant-ph) #Radiation Effects in Electronics
paper · pdf · doi:10.48550/arxiv.2111.13728
openalex publication_date 2021/11/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Quantum Error Correction (QEC) is essential for fault-tolerant quantum copmutation, and its implementation is a very sophisticated process involving both quantum and classical hardware. Formulating and verifying the decomposition of logical operations into physical ones is a challenge in itself. In this paper, we propose QECV, a verification framework that can efficiently verify the formal correctness of stabilizer codes, arguably the most important class of QEC codes. QECV first comes with a concise language, QECV-Lang, where stabilizers are treated as a first-class object, to represent QEC programs. Stabilizers are also used as predicates in our new assertion language, QECV-Assn, as logical and arithmetic operations of stabilizers can be naturally defined. We derive a sound quantum Hoare logic proof system with a set of inference rules for QECV to efficiently reason about the correctness of QEC programs. We demonstrate the effectiveness of QECV with both theoretical complexity analysis and in-depth case studies of two well-known stabilizer QEC codes, the repetition code and the surface code.