Qafny: A Quantum-Program Verifier
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2022
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866929412067295232 |
|---|---|
| author | Li, Liyi Zhu, Mingwei Cleaveland, Rance Nicolellis, Alexander Lee, Yi Chang, Le Wu, Xiaodi |
| author_facet | Li, Liyi Zhu, Mingwei Cleaveland, Rance Nicolellis, Alexander Lee, Yi Chang, Le Wu, Xiaodi |
| contents | Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2211_06411 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Qafny: A Quantum-Program Verifier Li, Liyi Zhu, Mingwei Cleaveland, Rance Nicolellis, Alexander Lee, Yi Chang, Le Wu, Xiaodi Quantum Physics Programming Languages Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm. |
| title | Qafny: A Quantum-Program Verifier |
| topic | Quantum Physics Programming Languages |
| url | https://arxiv.org/abs/2211.06411 |