计算机工程与应用 ›› 2010, Vol. 46 ›› Issue (8): 16-20.DOI: 10.3778/j.issn.1002-8331.2010.08.005

• 博士论坛 • 上一篇    下一篇

抽象解释理论框架及其应用

杨 波1,2,张明义3,谢 刚4   

  1. 1.贵州大学 计算机科学与信息学院,贵阳 550025
    2.贵阳学院 物理与电子信息科学系,贵阳 550005
    3.贵州科学院,贵阳 550001
    4.贵州师范大学 数学与计算机科学学院,贵阳 550001
  • 收稿日期:2009-11-26 修回日期:2010-01-13 出版日期:2010-03-11 发布日期:2010-03-11
  • 通讯作者: 杨 波

Abstract interpretation theory and its application

YANG Bo1,2,ZHANG Ming-yi3,XIE Gang4   

  1. 1.College of Computer Science and Information,Guizhou University,Guiyang 550025,China
    2.Department of Physics and Electronics Information Science,Guiyang College,Guiyang 550005,China
    3.Guizhou Academy of Science,Guiyang 550001,China
    4.College of Mathematics and Computer Science,Guizhou Normal University,Guiyang 550001,China
  • Received:2009-11-26 Revised:2010-01-13 Online:2010-03-11 Published:2010-03-11
  • Contact: YANG Bo

摘要: 在高度依赖计算机的现代社会,软件(特别是大型实时安全攸关软件)的可靠性成为计算机界和整个社会都非常关注的问题。现有的形式化软件验证工具都不得不通过近似来处理复杂问题中的计算,P.Cousot和R.Cousot提出的抽象解释作为一种在数学模型间进行可靠近似的理论,为各类自动验证工具中不同的近似方法建立起一个统一的形式化框架。抽象解释理论在程序分析和验证研究领域得到了广泛的关注与应用,其应用范围涵盖了程序静态分析、程序变换、程序调试、程序水印等方面。描述了基于程序不动点语义的抽象解释理论框架,并对其近年来的应用现状进行了较为全面的介绍,最后给出了抽象解释理论中尚存在的一些问题及可能的研究方向。

Abstract: In a highly computer-dependent society,reliability of software,especially of big real-time safety critical ones,gains far-ranging attention from computer community and the rest of the world.Existing tools for formal program verifying have to deal with complex computation through approximating to some extent.Presented by P.Cousot and R.Cousot,abstract interpretation is a theory for sound approximation between mathematic models,and constructs a unifying formal framework for different approximate methods of different program verification tools.Therefore,abstract interpretation is discussed and applied widely in several program analysis and verification fields,including static analysis,program transform,debugging,program watermarking,and so on.This paper first describes the theory framework of abstracting program’s fixpoint semantics,then introduces its state of the art and future challenges.

中图分类号: