Verification Logics for Quantum Programs
Logic in Computer Science
2019-04-10 v1 Emerging Technologies
Programming Languages
Abstract
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.
Cite
@article{arxiv.1904.04304,
title = {Verification Logics for Quantum Programs},
author = {Robert Rand},
journal= {arXiv preprint arXiv:1904.04304},
year = {2019}
}
Comments
Originally submitted in March 2016 as a qualifying examination (WPE-II) for the PhD program at the University of Pennsylvania