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

• 作者: 张明义 杨波 谢刚
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 语义 Galois连接 Widening算子 Narrowing算子 抽象解释
• 年，卷（期）: 2010,（8）
• 所属期刊栏目: 博士论坛
• 页码范围: 16-20,44
• 页数: 6页
• 分类号: TP311.1
• 字数: 6776字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2010.08.005

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谢刚	贵州师范大学数学与计算机科学学院	20	82	5.0	8.0
2	杨波	贵州大学计算机科学与信息学院	39	58	4.0	7.0
6	张明义		18	89	5.0	9.0