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 (12)
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Quantum algorithm for solving linear systems of equations
- Surface codes: Towards practical large-scale quantum computation
- Satellite-to-ground quantum key distribution
- A Quantum Approximate Optimization Algorithm
- tket : A Retargetable Compiler for NISQ Devices
- Resource-Aware Quantum Programming with General Recursion and Quantum Control
- A Lambda Calculus for Quantum Computation
- ScaffCC: Scalable Compilation and Analysis of Quantum Programs
- Generalized Flow and Determinism in Measurement-based Quantum Computation
- Certified Quantum Computation in Isabelle/HOL
- Quantum Hoare Type Theory