Quantum Programs Verification and Analysis

In the Quantum Programs Verification and Analysis project in VeriQ, we develop new theories and tools to verify the correctness and analyze the effectiveness of quantum programs. With the help of our original theoretical framework, high-level and large-scale quantum programs can be effectively verified and analyzed on both paper and classical computers.


We formalize quantum Hoare logic in Isabelle/HOL. In particular, we specify the syntax and denotational semantics of a simple model of quantum programs. Then, we write down the rules of quantum Hoare logic for partial correctness, and show the soundness and completeness of the resulting proof system. As an application, we verify the correctness of Grover’s algorithm.

See Isabelle AFP

[1] Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum hoare logic. In Computer Aided Verification - 31st International Conference, CAV 2019, volume 11562 of Lecture Notes in Computer Science, pages 187–207. Springer, 2019. [ DOI | http ]