Formal Verification of Quantum Programs: Theory, Tools and Challenges

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.

32 pages; changes to Sections 2, 3, 4, 5.5, Appendix

References in corpus (16)

• Supplementary information for "Quantum supremacy using a programmable superconducting processor"
• Quantum cryptography: Public key distribution and coin tossing
• Quantum algorithm for solving linear systems of equations
• Quantum computational advantage using photons
• Exponential algorithmic speedup by quantum walk
• A Deductive Verification Framework for Circuit-building Quantum Programs
• 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
• Proving Quantum Programs Correct
• Partial Equivalence Checking of Quantum Circuits
• Formal Methods for Quantum Programs: A Survey
• Quantum Algorithms and Oracles with the Scalable ZX-calculus
• An Algebraic Method to Fidelity-based Model Checking over Quantum Markov Chains
• 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