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