基于抽象解释的函数不变量正确性验证

• 作者: 刘久富 武书彦 苏青琴
• 来源期刊: 微电子学与计算机
• 关键词: 函数不变量 抽象解释 正确性验证 多项式关系
• 年，卷（期）: 2012,（10）
• 页码范围: 161-165
• 分类号: TP311
• 语种: 中文

摘要

函数不变量检测是提高软件质量的一种有效方法.针对检测方法可能带来无效的函数不变量的缺陷,提出一种以抽象解释理论为基础的函数不变量的正确性验证方法.首先将函数不变量转化成多项式关系;其次结合多项式程序与最弱前置条件抽象解释分析多项式关系正确性的判断依据;最后构造多项式关系算法,凭借得到的结果验证函数不变量正确与否.同时通过一个C程序中的函数不变量为例对该验证方法进行说明.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	武书彦	郑州牧业工程高等专科学校信息工程系	28	58	5.0	6.0
2	刘久富	南京航空航天大学自动化学院	53	207	8.0	11.0
3	苏青琴	南京航空航天大学自动化学院	4	5	2.0	2.0