Formal Methods for Quantum Programs: A Survey
arXiv:2109.06493
Abstract
While recent progress in quantum hardware open the door for significant speedup in certain key areas (cryptography, biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of such quantum programs is achallenge. Moreover, importing the testing and debugging practices at use in classical programming is extremely difficult in the quantum case, due to the destructive aspect of quantum measurement. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. Recent works initiate solutions for problems occurring at every stage of the development process: high-level program design, implementation, compilation, etc. We review the induced challenges for an efficient use of formal methods in quantum computing and the current most promising research directions.
References in corpus (41)
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Quantum Machine Learning
- The Security of Practical Quantum Key Distribution
- Quantum algorithm for solving linear systems of equations
- Surface codes: Towards practical large-scale quantum computation
- Decoy State Quantum Key Distribution
- The theory of variational hybrid quantum-classical algorithms
- A Quantum Adiabatic Evolution Algorithm Applied to Random Instances of an NP-Complete Problem
- Satellite-to-ground quantum key distribution
- A Quantum Approximate Optimization Algorithm
- Measurement-based quantum computation with cluster states
- Quantum algorithms for supervised and unsupervised machine learning
- ProjectQ: An Open Source Software Framework for Quantum Computing
- tket : A Retargetable Compiler for NISQ Devices
- Strawberry Fields: A Software Platform for Photonic Quantum Computing
- Resource-Aware Quantum Programming with General Recursion and Quantum Control
- Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning
- Quantum Error Correction
- A Lambda Calculus for Quantum Computation
- Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus
- Reducing T-count with the ZX-calculus
- ScaffCC: Scalable Compilation and Analysis of Quantum Programs
- Determinism in the one-way model
- Generalized Flow and Determinism in Measurement-based Quantum Computation
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- Volume and Quantizations
- A Verified Optimizer for Quantum Circuits
- The ZX calculus is a language for surface code lattice surgery
- An Introduction to Quantum Programming in Quipper
- Concrete resource analysis of the quantum linear system algorithm used to compute the electromagnetic scattering cross section of a 2D target
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Generators and relations for n-qubit Clifford operators
- Certified Quantum Computation in Isabelle/HOL
- The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects
- Formal Verification of Quantum Protocols
- Hypergraph Simplification: Linking the Path-sum Approach to the ZH-calculus
- A Finite Presentation of CNOT-Dihedral Operators
- A Theorem Prover for Quantum Hoare Logic and Its Applications
- Linear Dependent Type Theory for Quantum Programming Languages
- Quantum Hoare Type Theory