程序条件化用于软件模型检测中的状态空间缩减

• 作者: 张勇 张德运 肖健宇 郑卫斌
• 来源期刊: 西安交通大学学报
• 关键词: 程序条件化 软件模型检测 状态空间缩减 符号化执行 线性时序逻辑
• 年，卷（期）: 2006,（4）
• 所属期刊栏目: 专题研究
• 页码范围: 377-380
• 页数: 4页
• 分类号: TP311.1
• 语种: 中文
• DOI: 10.3321/j.issn:0253-987X.2006.04.002

摘要

针对软件模型检测中的状态爆炸问题,提出将程序条件化技术用于软件状态空间缩减的方案.以程序性质的线性时序逻辑公式可能出现的蕴涵式的前件作为条件化的约束条件,通过分析程序符号化执行语义,借助自动定理证明器,对语句的可达性条件进行逻辑推理,删除那些与性质的可满足性无关的语句,以达到程序精简的目的.理论分析和实验结果表明,条件化可以有效缩减程序状态空间,而且缩减后的程序模型保留了原程序中与所需验证的性质有关的所有信息,满足软件模型检测对状态缩减的安全性要求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	郑卫斌	西安交通大学电子与信息工程学院	23	135	7.0	11.0
3	肖健宇	西安交通大学电子与信息工程学院	13	83	6.0	8.0
7	张勇		1	3	1.0	1.0