将量子程序验证技术嵌入到 Dafny 语言中

《Proceedings of the ACM on Programming Languages》：Embedding Quantum Program Verification into Dafny

量子程序验证面临概率性和叠加性挑战，Qafny系统通过编译量子验证到Dafny，实现形式化验证并成功验证37个量子程序，是目前最广泛的量子程序形式化验证集合。

　　

摘要

尽管量子程序验证技术近年来有所发展，但它仍处于起步阶段。由于量子叠加的随机性和并行性，许多量子程序难以被验证。我们提出了Qafny^C这一系统，它将量子程序验证过程编译为成熟的经典程序验证工具Dafny，从而实现了量子程序的形式化验证。Qafny^C的核心思想是将量子程序验证与其执行过程分离，利用经典验证工具的优势在将经过验证的量子程序编译为可执行电路之前确保其正确性。通过使用Qafny^C，我们已经成功地将37个不同的量子程序的验证过程编译到了Dafny中。据我们所知，这是迄今为止形式化验证最完整的量子程序集合。