Formal Verification of Quantum Programs: Theory, Tools and Challenges
arXiv:2110.01320 · doi:10.1145/3624483
Abstract
Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.
arXiv comment32 pages; changes to Sections 2, 3, 4, 5.5, Appendix
References in corpus (34)
- Quantum Computing in the NISQ era and beyond
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
- Quantum cryptography: Public key distribution and coin tossing
- Quantum algorithm for solving linear systems of equations
- Quantum computational advantage using photons
- Quantum Chemistry in the Age of Quantum Computing
- Exponential algorithmic speedup by quantum walk
- Simulation of Electronic Structure Hamiltonians Using Quantum Computers
- Quantum advantage with shallow circuits
- Quantum Error Correction: An Introductory Guide
- Improved classical simulation of quantum circuits dominated by Clifford gates
- Interacting Quantum Observables: Categorical Algebra and Diagrammatics
- Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
- Quipper: A Scalable Quantum Programming Language
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- PyZX: Large Scale Automated Diagrammatic Reasoning
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Quantum Relational Hoare Logic
- Quantum Hoare logic with classical variables
- Tools for Quantum Computing Based on Decision Diagrams
- Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
- Certified Quantum Computation in Isabelle/HOL
- QDB: From Quantum Algorithms Towards Correct Quantum Programs
- Proving Quantum Programs Correct
- A Simplified Stabilizer ZX-calculus
- Partial Equivalence Checking of Quantum Circuits
- CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
- Authenticated teleportation and verification in a noisy network
- Quantum Temporal Logic
- Formal Methods for Quantum Programs: A Survey
- An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains
- Quantum Algorithms and Oracles with the Scalable ZX-calculus
- Quantum projective measurements and the CHSH inequality in Isabelle/HOL
Cited by in corpus (10)
- Efficient Formal Verification of Quantum Error Correcting Programs
- Rotational Abstractions for Verification of Quantum Fourier Transform Circuits
- Blockchain Security Risk Assessment in Quantum Era, Migration Strategies and Proactive Defense
- On the need for effective tools for debugging quantum programs
- Benchmarking Quantum Computers: Towards a Standard Performance Evaluation Approach
- Quantum Circuit Mutants: Empirical Analysis and Recommendations
- Automated Verification of Silq Quantum Programs using SMT Solvers
- Automating Equational Proofs in Dirac Notation
- A Practical Quantum Hoare Logic with Classical Variables, I
- Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs