Verification Logics for Quantum Programs
Robert Rand
TL;DR
This paper surveys various Hoare logics for quantum programs, comparing their foundations, expressivity, and practical usability through case verification of the Deutsch-Jozsa Algorithm.
Contribution
It provides a comparative analysis of three quantum Hoare logics, highlighting their differences and practical applications in quantum program verification.
Findings
Different logics vary in expressivity and usability
All logics successfully verify the Deutsch-Jozsa Algorithm
The survey guides future development of quantum verification tools
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Computing Algorithms and Architecture · Computability, Logic, AI Algorithms · Logic, programming, and type systems