Proving Quantum Programs Correct

Abstract

As quantum computing progresses steadily from theory into practice, programmers will face a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Grover's algorithm and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.

version 4 updated DOI (paper content is the same); version 3 (final version) has updated formatting and improved writing; version 2 includes updated acknowledgments and a new appendix with simple SQIR example programs

References in corpus (4)

• Quantum algorithm for solving linear systems of equations
• Resource-Aware Quantum Programming with General Recursion and Quantum Control
• ReQWIRE: Reasoning about Reversible Quantum Circuits
• Certified Quantum Computation in Isabelle/HOL

Cited by in corpus (7)

• Formal Verification of Quantum Programs: Theory, Tools and Challenges
• symQV: Automated Symbolic Verification of Quantum Programs
• Symbolic Execution for Quantum Error Correction Programs
• On the need for effective tools for debugging quantum programs
• Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation
• Verification of Quantum Systems using Barrier Certificates
• Automating Equational Proofs in Dirac Notation