Conference PaperQafny: A Quantum-Program VerifierLi, Liyi; Zhu, Mingwei; Cleaveland, Rance; Nicolellis, Alexander; Lee, Yi; Chang, Le; Wu, XiaodiAldrich, Jonathan; Salvaneschi, GuidoBecause 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.Schloss Dagstuhl – Leibniz-Zentrum für Informatik2024-01-0110560374313313-3131868-8969978-3-95977-341-6https://doi.org/10.4230/LIPIcs.ECOOP.2024.242330974Quantum ComputingAutomated VerificationSeparation LogicTheory of computation → Program verificationTheory of computation → Quantum information theory31 pages831757 bytesapplication/pdfCreative Commons Attribution 4.0 International license; info:eu-repo/semantics/openAccessNational Science Foundation