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

摘要：

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

关键词：软件模型检测、状态-迁移模型、状态爆炸、程序条件化、自动定理证明

所属期刊栏目：32

分类号：TP311.1(计算技术、计算机技术)

资助基金：国家自然科学基金60403028

在线出版日期：2006-11-07（万方平台首次上网日期，不代表论文的发表时间）

页数：共3页

页码：51-53