Toward Automatic Verification of Quantum Programs

Abstract

This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper.

References in corpus (5)

• Distributed quantum computation via optical fibres
• Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
• ScaffCC: Scalable Compilation and Analysis of Quantum Programs
• Arithmetic on a Distributed-Memory Quantum Multicomputer
• Provable Quantum Advantage in Randomness Processing

Cited by in corpus (6)

• A Deductive Verification Framework for Circuit-building Quantum Programs
• Quantum Hoare logic with classical variables
• Verification of Distributed Quantum Programs
• On the need for effective tools for debugging quantum programs
• Verifying Quantum Phase Estimation (QPE) using Prove-It
• A Practical Quantum Hoare Logic with Classical Variables, I