用于克服程序状态空间爆炸的条件化预处理

• 作者: 张德运 肖健宇 董皓 陈海诠
• 来源期刊: 计算机工程
• 学科: 工学
• 关键词: 软件模型检测 状态-迁移模型 状态爆炸 程序条件化 自动定理证明
• 年，卷（期）: 2006,（19）
• 所属期刊栏目: 软件技术与数据库
• 页码范围: 51-53
• 页数: 3页
• 分类号: TP311.1
• 字数: 5149字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-3428.2006.19.019

摘要

提出用条件化技术对程序进行预处理的方案,以克服软件模型检测中状态空间爆炸问题.以程序性质公式中蕴涵式的前件作为约束条件,通过对程序符号化执行后各控制点的路径条件进行逻辑推理,删除那些对性质检测无关的语句.理论分析和实验结果表明,条件化可以有效缩减程序状态空间,并且满足软件模型检测对状态缩减的安全性要求.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张德运	西安交通大学电子与信息工程学院	184	2190	23.0	37.0
2	肖健宇	湖南涉外经济学院计算机系	4	21	2.0	4.0
6	陈海诠	西安交通大学电子与信息工程学院	8	67	5.0	8.0
7	董皓	西安交通大学电子与信息工程学院	12	83	6.0	9.0