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

摘要：

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

关键词：程序条件化、软件模型检测、状态空间缩减、符号化执行、线性时序逻辑

所属期刊栏目：40

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

资助基金：中国科学院资助项目60403028

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

页数：共4页

页码：377-380