软件所量子软件团队推出国际首个量子程序证明工具
2019/3/31 9:49:52 中国科学院软件研究所

     为了保证程序的正确性及应用系统的安全性，程序测试、分析与验证在经典计算机科学占有重要的地位。量子世界与经典世界有着本质的不同，人类的直觉在处理量子世界中的问题时，往往容易做出错误的判断。因而，量子程序设计更加容易出错。

     近日，软件所量子软件团队詹博华博士及博士生刘君毅等推出国际首个量子程序证明工具QHLProver。QHLProver是基于开源定理证明器Isabelle/ HOL的量子算法正确性推理工具。它的逻辑基础是本团队提出的量子Hoare逻辑(quantumHoare logic，QHL)。

     量子程序证明工具QHLProver 网址：

     http://qsoft.ios.ac.cn/tools/qhlprover/

     https://www.isa-afp.org/entries/QHLProver.html

     文章来源:计算机科学国家重点实验室

    http://weixin.100md.com
返回 中国科学院软件研究所 返回首页 返回百拇医药