{"id":"arxiv:2501.14380","kind":"article","title":"Verifying Fault-Tolerance of Quantum Error Correction Codes","authors":["Kean Chen","Yuhao Liu","Wang Fang","Jennifer Paykin","Xin-Chuan Wu","Albert Schmitz","Steve Zdancewic","Gushu Li"],"author_count":8,"year":2025,"published":"2025-01-24","venue":"International Conference on Computer Aided Verification (CAV 2025), pp. 3-27","cited_by":7,"doi":"10.1007/978-3-031-98685-7_1","arxiv_id":"2501.14380","nct_id":null,"source_url":"https://arxiv.org/abs/2501.14380","archive_url":"https://space-kitty.com/papers/arxiv:2501.14380","updated":"2025-06-07","pmid":null,"pmcid":null,"openalex_id":"W4412544349","pdf_url":"https://arxiv.org/pdf/2501.14380","abstract":"Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":null,"categories":["quant-ph","cs.PL"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"quantum-error-correction","name":"Quantum Error Correction & Fault Tolerance","domain_slug":"quantum-computing"}],"cited_in_dossiers":[]}