基于Isabelle定理证明器算法程序的形式化验证

摘要：

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到”提高验证效率和保证算法程序高可信”的目标,具有很好的实用价值。

关键词： 形式化验证 机械证明 算法程序 定理证明器

作者: 游珍 薛锦云

作者单位: 江西师范大学省高性能计算技术重点实验室,江西,南昌,330022 江西师范大学省高性能计算技术重点实验室,江西,南昌,330022;中国科学院软件研究所,北京,100190

会议类型: 国内会议

会议名称: 2009年全国理论计算机科学学术年会

会议地点: 哈尔滨

会议语种:中文

页码: 85-89

在线出版日期: 2009-08-07（万方平台首次上网日期，不代表论文的发表时间）