Reasoning about Grover's Quantum Search Algorithm using Probabilistic wp

Michael Butler, Pieter Hartel

Grover's search algorithm is designed to be executed on a quantum mechanical computer. In this paper, the probabilistic wp-calculus is used to model and reason about Grover's algor…