A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
It is well-known that quantum programs are not only complicated to write but also tedious to verify due to their enormous state-space and the sophisticated mathematics beneath. In this work, we propose a Hoare-style inference framework to verify quantum programs. We infuse separation logic in our fr...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | text |
| Language: | English |
| Published: |
Institutional Knowledge at Singapore Management University
2022
|
| Subjects: | |
| Online Access: | https://ink.library.smu.edu.sg/sis_research/6919 https://ink.library.smu.edu.sg/context/sis_research/article/7922/viewcontent/3498697_pvoa_cc_by.pdf |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Institution: | Singapore Management University |
| Language: | English |
| Summary: | It is well-known that quantum programs are not only complicated to write but also tedious to verify due to their enormous state-space and the sophisticated mathematics beneath. In this work, we propose a Hoare-style inference framework to verify quantum programs. We infuse separation logic in our framework and invent the $\hoarule{qframe}$ rule, the quantum counterpart of the frame rule, to support local reasoning of quantum programs. The design of our framework is planned with a mindset for intuition and human-readability, using vectors in Dirac notation for reasoning instead of the orthodox matrix representation as in existing approaches. For evaluation, we apply our framework to verify various quantum programs such as Deutsch-Jozsa’s algorithm and Grover’s algorithm. |
|---|