量子程序的形式化方法：一项调查
摘要：量子计算机硬件的最新进展为某些关键领域（加密学、生物学、化学、优化、机器学习等）的显著加速打开了大门，但量子算法仍然很难正确实现，并且验证此类量子程序是个挑战。此外，由于量子测量的破坏性特性，将经典编程中使用的测试和调试方法引入量子情况非常困难。作为替代策略，形式化方法在量子软件的新兴领域中将发挥决定性作用。最近的研究已经在开发过程的每个阶段提供了解决方案：高级程序设计、实现、编译等。我们回顾了在量子计算中有效使用形式化方法时所面临的挑战，以及当前最有前景的研究方向。
作者：Christophe Chareton, S''ebastien Bardin, Dongho Lee, Beno^it Valiron, Renaud Vilmart, Zhaowei Xu
论文ID：2109.06493
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-04-11