Verification of Concurrent Quantum Protocols by Equivalence Checking

Simon Gay ( Department of Computing Science, University of Glasgow )

We present a tool which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. We work in the stabilizer formalism, for which there are efficient simulation algorithms. In particular, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of the concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. Despite the limitations of the stabilizer formalism, equivalence checking can be used to verify several interesting quantum protocols. Finally, we describe recent work on extending this approach beyond the stabilizer formalism.