Verifying the Steane code with Quantomatic
This work addresses verification of quantum error-correcting codes for researchers in quantum computing, but it is incremental as it applies an existing tool to a new, larger case.
The paper tackled verifying the correctness of Steane's 7-qubit error-correcting code using the tool Quantomatic, achieving a partially mechanized proof that represents the largest and most complicated verification task performed with Quantomatic to date.
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.