Publication Type
Journal Article
Version
publishedVersion
Publication Date
1-2022
Abstract
It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space explosion problem for quantum reasoning, we propose a Hoare-style inference framework that supports local reasoning for quantum programs. By providing a quantum interpretation of the separating conjunction, we are able to infuse separation logic into our framework and apply local reasoning using a quantum frame rule that is similar to the classical frame rule. For evaluation, we apply our framework to verify various quantum programs including Deutsch–Jozsa’s algorithm and Grover's algorithm.
Keywords
Formal Semantics, Quantum Computing, Verification
Discipline
Software Engineering | Theory and Algorithms
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the ACM on Programming Languages
Volume
6
Issue
POPL
First Page
1
Last Page
27
Identifier
10.1145/3498697
Publisher
ACM
Citation
LE, Xuan Bach; LIN, Shang-Wei; SUN, Jun; and SANAN, David.
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic. (2022). Proceedings of the ACM on Programming Languages. 6, (POPL), 1-27.
Available at: https://ink.library.smu.edu.sg/sis_research/6941
Copyright Owner and License
Authors
Creative Commons License
This work is licensed under a Creative Commons Attribution 4.0 International License.
Additional URL
https://doi.org/10.1145/3498697