基于抽象域和数值熵协同的数值程序分析

• 作者: 刘久富 王正谦 马国富
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: 数值程序分析 正确性 抽象解释 数值信息熵
• 年，卷（期）: 2015,（6）
• 页码范围: 55-58,119
• 页数: 5页
• 分类号: TP311
• 字数: 4294字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.1305-0529

摘要

在软件日益丰富的信息时代，程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析，提取不变量的抽象域区间；在抽象域区间上进行数值熵运算；运行程序获取数值变量的实际取值，计算数值熵；将抽象域区间数值熵和实际数值熵信息进行对比分析，准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围，而引入数值熵算法，在取值范围的基础上对程序静态分析的准确性进一步检验，同时也做到了对程序的正确性验证。通过C语言程序实例，对抽象解释基础上的熵值分析方法进行了验证，证明了该分析方法的可行性和正确性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	马国富	安阳工学院计算机科学与信息工程学院	13	21	2.0	4.0
2	刘久富	南京航空航天大学自动化学院	53	207	8.0	11.0
3	王正谦	南京航空航天大学自动化学院	4	1	1.0	1.0