Verifying the Steane code with Quantomatic
Ross Duncan (University of Strathclyde, Glasgow, UK), Maxime Lucas, (Universit\'e Libre de Bruxelles, Brussels, Belgium)
TL;DR
This paper presents a mechanized proof of the correctness of Steane's 7-qubit error correcting code using Quantomatic, demonstrating its capability to handle complex quantum verification tasks.
Contribution
First large-scale verification of Steane's code using Quantomatic, showcasing its potential for verifying complex quantum error correction codes.
Findings
Successful mechanized proof of Steane's code correctness
Demonstrates Quantomatic's capacity for complex quantum verification
Establishes a new benchmark for automated quantum code verification
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.