00869nas a2200097 4500008004100000245004500041210004500086520058600131100001700717856003700734 2019 eng d00aVerification Logics for Quantum Programs0 aVerification Logics for Quantum Programs3 a
We survey the landscape of Hoare logics for quantum programs. We review three papers: "Reasoning about imperative quantum programs" by Chadha, Mateus and Sernadas; "A logic for formal verification of quantum programs" by Yoshihiko Kakutani; and "Floyd-hoare logic for quantum programs" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.
1 aRand, Robert uhttps://arxiv.org/abs/1904.04304