



01569nas a2200169   4500008004100000245008700041210006900128260001400197520105800211100001301269700001701282700002201299700001201321700001401333700001501347856003701362       2023                        eng d00aQafny: Quantum Program Verification Through Type-guided Classical Separation Logic0 aQafny Quantum Program Verification Through Typeguided Classical   c7/12/20233 a<p>Formal verification has been proven instrumental to ensure that quantum programs implement their specifications but often requires a significant investment of time and labor. To address this challenge, we present Qafny, an automated proof system designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. By modeling these operations as proof rules within a classical separation logic framework, Qafny provides automated support for the reasoning process that would otherwise be tedious and time-consuming. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs both into the Dafny programming language and into executable quantum circuits. Using Qafny, we demonstrate how to efficiently verify prominent quantum algorithms, including quantum-walk algorithms, Grover&#39;s search algorithm, and Shor&#39;s factoring algorithm, with significantly reduced human efforts.</p>1 aLi, Liyi1 aZhu, Mingwei1 aCleaveland, Rance1 aLee, Yi1 aChang, Le1 aWu, Xiaodi  uhttps://arxiv.org/abs/2211.06411