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

• 作者: 游珍 薛锦云
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 形式化验证 定理机械证明 Dijkstra最弱前置谓词理论 PAR方法 算法程序 定理证明器
• 年，卷（期）: 2009,（10）
• 所属期刊栏目: 软件工程
• 页码范围: 85-89
• 页数: 5页
• 分类号: TP311
• 字数: 4515字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2009.10.024

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	薛锦云	江西师范大学省高性能计算技术重点实验室	77	745	15.0	23.0
3	游珍	江西师范大学省高性能计算技术重点实验室	5	45	5.0	5.0