Title: Verifying Quantum Programs: From Quipper to QPMC,
Abstract: In this paper we present a translation from the quantum programming language
Quipper to the QPMC model checker, with the main aim of verifying Quipper
programs. Quipper is an embedded functional programming language for quantum
computation. It is above all a circuit description language, for this reason it
uses the vector state formalism and its main purpose is to make circuit
implementation easy providing high level operations for circuit manipulation.
Quipper provides both an high-level circuit building interface and a simulator.
QPMC is a model checker for quantum protocols based on the density matrix
formalism. QPMC extends the probabilistic model checker IscasMC allowing to
formally verify properties specified in the temporal logic QCTL on Quantum
Markov Chains. We implemented and tested our translation on several quantum
algorithms, including Grover's quantum search.