Verification of Nondeterministic Quantum Programs

TL;DR

This paper develops Hoare-type logic systems for verifying nondeterministic quantum programs, extending termination analysis to correctness verification, and demonstrates their application on quantum algorithms with a prototype proof assistant.

Contribution

It introduces sound and relatively complete Hoare logic systems for nondeterministic quantum programs, advancing verification methods beyond termination analysis.

Findings

Logic systems are sound and relatively complete.

Applied verification to quantum algorithms like error correction and Deutsch.

Prototype proof assistant supports automated reasoning.

Abstract

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and the termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed, which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms, such as quantum error correction scheme, the Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.