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

Abstract interpretation theory and its application

作　　者：杨波[1,2] 张明义[3] 谢刚[4] 

机构地区：[1]贵州大学计算机科学与信息学院,贵阳550025 [2]贵阳学院物理与电子信息科学系,贵阳550005 [3]贵州科学院,贵阳550001 [4]贵州师范大学数学与计算机科学学院,贵阳550001

出　　处：《计算机工程与应用》2010年第8期16-20,44,共6页Computer Engineering and Applications

基　　金：国家自然科学基金Grant No.90718009;贵州省科学技术基金(No.[2009]2119);贵州省教育厅自然科学基金 Grant No.(2009)0061~~

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

关 键 词：语义 Galois连接 widening算子 Narrowing算子 抽象解释 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]