论文标题
QAFNY：量子编程验证者
Qafny: A Quantum-Program Verifier
论文作者
论文摘要
由于量子程序的概率/非确定性行为，强烈建议对它们进行正式验证以确保它们正确实施其规格。然而，传统上也需要大量努力。为了应对这一挑战，我们提出了基于程序验证者dafny的自动证明系统Qafny，并旨在验证量子程序。 QAFNY以核心使用类型引导的量子证明系统，该系统将量子操作转换为在经典分离逻辑框架内建模的经典数组操作。我们证明了证明系统的健全性和完整性，并实施了原型编译器，该原型编译器将QAFNY程序和规格转换为DAFNY，以进行自动验证。然后，我们说明了Qafny自动化功能在有效验证重要量子算法的实用性，包括量子 - 步行算法，Grover的算法和Shor的算法。
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.
