量子程序验证

来源：软件学报杂志2018年第4期北京时间：

作者：冯元,应明生

单位：冯元，University of Technology Sydney, Australia;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 10019011,应明生，University of Technology Sydney, Australia;计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;清华大学 计算机系, 北京 10008402

摘要：量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5~10年内实现.可以想见，到那时候，量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而，由于量子信息的不可克隆性和纠缠的非局域作用等量子特征，如何设计正确、高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法，特别是模型检测技术，已在经典软件设计和系统建模方面被证明行之有效，因此量子软件的形式化验证也开始受到越来越多的关注.从量子顺序程序验证和量子通信协议验证两方面，对近年来国内外学者，尤其对University of Technology Sydney和清华大学的研究组在该研究领域取得的一些成果进行了系统的总结.最后，对未来可能的研究方向和面临的挑战进行了简单展望.

关键词：量子计算;程序验证;模型检测;通信协议验证

基金资助：中国科学院前沿科学重点研究计划（QYZDJ-SSW-SYS003）；中国科学院、国家外国专家局创新团队国际合作伙伴计划