Verifying the Steane code with Quantomatic
arXiv:1306.4532 · doi:10.4204/EPTCS.171.4
Abstract
In this paper we give a partially mechanized proof of the correctness of Steane's 7-qubit error correcting code, using the tool Quantomatic. To the best of our knowledge, this represents the largest and most complicated verification task yet carried out using Quantomatic.
In Proceedings QPL 2013, arXiv:1412.7917
References in corpus (1)
Cited by in corpus (22)
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- The ZX calculus is a language for surface code lattice surgery
- The ZX-calculus is incomplete for quantum mechanics
- A universal completion of the ZX-calculus
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning
- Reconstructing quantum theory from diagrammatic postulates
- Optimising Clifford Circuits with Quantomatic
- ZX-calculus for the working quantum computer scientist
- Graphical Structures for Design and Verification of Quantum Error Correction
- Verifying the Smallest Interesting Colour Code with Quantomatic
- A ZX-Calculus with Triangles for Toffoli-Hadamard, Clifford+T, and Beyond
- Completeness of the ZX-Calculus
- Pauli Fusion: a Computational Model to Realise Quantum Transformations from ZX Terms
- Qutrit ZX-calculus is Complete for Stabilizer Quantum Mechanics
- Hybrid quantum-classical circuit simplification with the ZX-calculus
- Reasoning with !-Graphs
- The Qupit Stabiliser ZX-travaganza: Simplified Axioms, Normal Forms and Graph-Theoretic Simplification
- Normalization for planar string diagrams and a quadratic equivalence algorithm
- Graphical CSS Code Transformation Using ZX Calculus
- Picturing Counting Reductions with the ZH-Calculus
- Shaded Tangles for the Design and Verification of Quantum Programs (Extended Abstract)
- Shaded tangles for the design and verification of quantum circuits