



@article {3314,
	title = {Qafny: Quantum Program Verification Through Type-guided Classical Separation Logic},
	year = {2023},
	month = {7/12/2023},
	abstract = {<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>},
	url = {https://arxiv.org/abs/2211.06411},
	author = {Liyi Li and Mingwei Zhu and Rance Cleaveland and Yi Lee and Le Chang and Xiaodi Wu}
}
