文件比较算法fcomp在Isabelle/HOL中的验证
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

基金项目:

江苏省自然科学基金(BK20130070)


Verification of File Comparison Algorithm fcomp in Isabelle/HOL
Author:
Affiliation:

Fund Project:

Natural Science Foundation of Jiangsu Province of China (BK20130070)

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    Being unbound to the state space size, mechanical theorem proving is an important method in ensuring software's correctness and avoiding serious damage from program bugs. File comparison algorithms constitute a large family of algorithms which find wide range of application domains including bio-informatics, information retrieval and network security. This paper presents a work on formalization of fcomp, an efficient line oriented file comparison algorithm suggested by Miller and Myers in 1985, in the interactive theorem prover Isabelle/HOL. A small bug in fcomp's bound variable iteration is identified, and the termination and correctness of the modified algorithm is established. Formal analysis of time complexity is also performed which coincides with the algorithm designers' own results. The presented work lays a valuable foundation for subsequent formal checking of other file comparison algorithms.

    参考文献
    相似文献
    引证文献
引用本文

宋丽华,王海涛,季晓君,张兴元.文件比较算法fcomp在Isabelle/HOL中的验证.软件学报,2017,28(2):203-215

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2015-11-21
  • 最后修改日期:2016-03-22
  • 录用日期:
  • 在线发布日期: 2017-01-24
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号