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 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...

Full description

Saved in:
Bibliographic Details
Main Authors: LE, Xuan Bach, LIN, Shang-Wei, SUN, Jun, SANAN, David
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2022
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/6941
https://ink.library.smu.edu.sg/context/sis_research/article/7944/viewcontent/3498697_pvoa.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-7944
record_format dspace
spelling sg-smu-ink.sis_research-79442024-07-30T08:36:11Z A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic LE, Xuan Bach LIN, Shang-Wei SUN, Jun SANAN, David 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. 2022-01-01T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/6941 info:doi/10.1145/3498697 https://ink.library.smu.edu.sg/context/sis_research/article/7944/viewcontent/3498697_pvoa.pdf http://creativecommons.org/licenses/by/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Formal Semantics Quantum Computing Verification Software Engineering Theory and Algorithms
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Formal Semantics
Quantum Computing
Verification
Software Engineering
Theory and Algorithms
spellingShingle Formal Semantics
Quantum Computing
Verification
Software Engineering
Theory and Algorithms
LE, Xuan Bach
LIN, Shang-Wei
SUN, Jun
SANAN, David
A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
description 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.
format text
author LE, Xuan Bach
LIN, Shang-Wei
SUN, Jun
SANAN, David
author_facet LE, Xuan Bach
LIN, Shang-Wei
SUN, Jun
SANAN, David
author_sort LE, Xuan Bach
title A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
title_short A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
title_full A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
title_fullStr A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
title_full_unstemmed A Quantum interpretation of separating conjunction for local reasoning of Quantum programs based on separation logic
title_sort quantum interpretation of separating conjunction for local reasoning of quantum programs based on separation logic
publisher Institutional Knowledge at Singapore Management University
publishDate 2022
url https://ink.library.smu.edu.sg/sis_research/6941
https://ink.library.smu.edu.sg/context/sis_research/article/7944/viewcontent/3498697_pvoa.pdf
_version_ 1814047733928951808