



00869nas a2200097   4500008004100000245004500041210004500086520058600131100001700717856003700734       2019                        eng d00aVerification Logics for Quantum Programs0 aVerification Logics for Quantum Programs3 a<p>We survey the landscape of Hoare logics for quantum programs. We review three papers: &quot;Reasoning about imperative quantum programs&quot; by Chadha, Mateus and Sernadas; &quot;A logic for formal verification of quantum programs&quot; by Yoshihiko Kakutani; and &quot;Floyd-hoare logic for quantum programs&quot; 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.</p>1 aRand, Robert  uhttps://arxiv.org/abs/1904.04304