文献类型：期刊文章

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

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

出　　处：《计算机工程与应用》

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

年　　份：2010

卷　　号：46

期　　号：8

起止页码：16-20

语　　种：中文

收录情况：AJ、BDHX、BDHX2008、CSA、CSA-PROQEUST、CSCD、CSCD2011_2012、IC、INSPEC、JST、RCCSE、ZGKJHX、核心刊

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

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

分 类 号：TP311.1]