基于最弱前置条件的程序正确性分析

• 作者: 侯春燕 王劲松 郭莎莎
• 来源期刊: 高技术通讯
• 关键词: 程序正确性 最弱前置条件 静态分析 路径扩展 程序切片技术
• 年，卷（期）: 2019,（6）
• 所属期刊栏目: 计算机与通信技术
• 页码范围: 556-563
• 页数: 8页
• 字数: 5018字
• 语种: 中文
• DOI: 10.3772/j.issn.1002-0470.2019.06.005

摘要

随着软件的不断更新迭代,软件正确性检测的必要性愈加凸显,软件正确性检测的处理时间直接决定软件的维护成本.动态测试的断言编写和静态分析的符号执行均针对程序正确性进行优化完善,但分析结果易出现路径缺失甚至错误无法识别等问题.现有验证方法在路径扩展时易生成较多无用路径,且针对性不强,因此有必要研究一种更为可靠的方案.本文采用最弱前置条件对软件可行性加以分析,对程序执行语义正确建模,使用程序切片技术预处理程序代码,并根据层级结构存储节点及其子程序.实验结果表明,该方法可以有效减小静态分析对程序状态抽象操作带来的验证精度损耗,且能够遍历求解出程序的所有可能路径,并通过分组标出条件表达式的结论真假值,以此验证路径正确性,同时可对高复杂的程序代码进行有效的正确性分析.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王劲松	天津理工大学计算机科学与工程学院	35	218	9.0	13.0
2	郭莎莎	天津理工大学计算机科学与工程学院	1	0	0.0	0.0
3	侯春燕	天津理工大学计算机科学与工程学院	4	1	1.0	1.0