Automated Verification of Silq Quantum Programs using SMT Solvers
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909310510956544 |
|---|---|
| author | Lewis, Marco Zuliani, Paolo Soudjani, Sadegh |
| author_facet | Lewis, Marco Zuliani, Paolo Soudjani, Sadegh |
| contents | We present SilVer (Silq Verification), an automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing. The goal of the verification is to ensure correctness of the Silq quantum program against user-defined specifications using SMT solvers. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations, allowing for control of quantum operations using both classical and quantum conditions. Additionally, users can employ measurement flags within the specification to easily specify conditions that measurement results require to satisfy for being a valid behavior. We provide case studies on the verification of generating entangled states and multiple oracle-based algorithms. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_03119 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Automated Verification of Silq Quantum Programs using SMT Solvers Lewis, Marco Zuliani, Paolo Soudjani, Sadegh Quantum Physics Logic in Computer Science Software Engineering We present SilVer (Silq Verification), an automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing. The goal of the verification is to ensure correctness of the Silq quantum program against user-defined specifications using SMT solvers. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations, allowing for control of quantum operations using both classical and quantum conditions. Additionally, users can employ measurement flags within the specification to easily specify conditions that measurement results require to satisfy for being a valid behavior. We provide case studies on the verification of generating entangled states and multiple oracle-based algorithms. |
| title | Automated Verification of Silq Quantum Programs using SMT Solvers |
| topic | Quantum Physics Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2406.03119 |