文件比较算法fcomp在Isabelle/HOL中的验证

• 作者: 季晓君 宋丽华 张兴元 王海涛
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 文件比较算法 fcomp 交互式定理证明 Isabelle/HOL
• 年，卷（期）: 2017,（2）
• 所属期刊栏目: 算法设计与分析
• 页码范围: 203-215
• 页数: 13页
• 分类号: TP301
• 字数: 11143字
• 语种: 中文
• DOI: 10.13328/j.cnki.j0s.005098

摘要

基于机器定理证明的形式验证技术不受状态空间限制,是保证软件正确性、避免因潜在软件缺陷带来严重损失的重要方法.文件比较算法(file comparison algorithm)是一类成员众多,应用极为广泛,跨越生物信息学、情报检索、网络安全等多个应用领域的基础算法,在交互式定理证明器Isabelle/HOL中对Miller和Myers在1985年提出的基于行的文件比较算法fcomp做了形式化,改正了算法关于边界变量迭代的一个小错误,证明了改正后算法的可终止性和正确性;对算法时间复杂性做了完全形式化的分析,印证了算法的非形式化分析结论,为今后更多文件比较算法的形式验证提供了可供借鉴的经验.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王海涛	解放军理工大学信息管理中心	265	2291	25.0	40.0
2	宋丽华	解放军理工大学指挥信息系统学院	73	479	11.0	19.0
3	张兴元	解放军理工大学指挥信息系统学院	14	20	2.0	3.0
4	季晓君	解放军理工大学指挥信息系统学院	5	34	3.0	5.0