Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2409.10153 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910605260095488 |
|---|---|
| author | Su, Bonan Zhou, Li Feng, Yuan Ying, Mingsheng |
| author_facet | Su, Bonan Zhou, Li Feng, Yuan Ying, Mingsheng |
| contents | We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations, where allocation statements follow a dirty pattern, meaning that newly allocated qubits can nondeterministically assume arbitrary initial states. To thoroughly characterize heap manipulations in the quantum setting, we develop a quantum BI-style logic that includes interpretations for separating implication ($-\mkern-3mu*$) and separating conjunction ($*$). We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs and present a quantum separation logic which is sound and relatively complete. Finally, we apply our framework to verify the correctness of various practical quantum programs and to prove the correct usage of dirty ancilla qubits. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_10153 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | BI-based Reasoning about Quantum Programs with Heap Manipulations Su, Bonan Zhou, Li Feng, Yuan Ying, Mingsheng Quantum Physics We provide well-founded semantics for a quantum programming language Qwhile-hp with heap manipulations, where allocation statements follow a dirty pattern, meaning that newly allocated qubits can nondeterministically assume arbitrary initial states. To thoroughly characterize heap manipulations in the quantum setting, we develop a quantum BI-style logic that includes interpretations for separating implication ($-\mkern-3mu*$) and separating conjunction ($*$). We then adopt this quantum BI-style logic as an assertion language to reason about heap-manipulated quantum programs and present a quantum separation logic which is sound and relatively complete. Finally, we apply our framework to verify the correctness of various practical quantum programs and to prove the correct usage of dirty ancilla qubits. |
| title | BI-based Reasoning about Quantum Programs with Heap Manipulations |
| topic | Quantum Physics |
| url | https://arxiv.org/abs/2409.10153 |