Toward Automatic Verification of Quantum Programs

TL;DR

This paper explores a program logic framework for verifying quantum programs, including Hoare logic, invariants, and termination, with new proof techniques and future research directions.

Contribution

It introduces quantum Hoare logic, proof outlines, and auxiliary rules, advancing formal verification methods for quantum programming.

Findings

Development of quantum Hoare logic for program verification

Introduction of proof outlines for quantum programs

Proposals for future research in quantum program verification

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.