支持抽象解释的静态分析方法的形式化体系研究

• 作者: 丁泽文 张弛 黄志球
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 形式化方法 静态分析 抽象解释 可配置程序分析
• 年，卷（期）: 2017,（12）
• 所属期刊栏目: 软件与数据库技术
• 页码范围: 126-130,155
• 页数: 6页
• 分类号: TP311
• 字数: 7044字
• 语种: 中文
• DOI: 10.11896/j.issn.1002-137X.2017.12.025

摘要

在安全关键领域中,如何保证软件的安全性已经成为了一个广受关注的重要课题.静态程序分析是一类十分有效的程序自动化验证方法.基于抽象解释的静态分析技术在验证软件的非功能性安全属性上表现十分突出.可配置程序分析(Configurable Program Analysis,CPA)是一种通用静态分析方法形式化体系,旨在用一种形式化体系对静态分析的分析阶段进行建模.使用CPA对基于抽象解释的静态分析进行建模,给出如何使用CPA形式化体系描述基于抽象解释的静态分析,给出了从待分析程序到CPA形式化体系的转换规则;提供了一种在安全关键性领域中的软件正确性自动验证方法,为基于抽象解释的静态分析工具的实现提供了一种可行方案.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	张弛	南京航空航天大学计算机科学与技术学院	9	8	2.0	2.0
3	丁泽文	南京航空航天大学计算机科学与技术学院	4	2	1.0	1.0