Abstract: A scheme of applying technique of conditioning to preprocess a program is proposed to alleviate the problem of state space explosion faced by software model checking. It takes the antecedent of an implication form in linear temporal logic formula of program properties as the condition of program conditioning, reasons the path condition of each control point of the program after symbolic execution, and deletes the irrelevant statements with respect to the verification of the program properties. Theoretical analysis and experiments show that the scheme can effectively reduce a program’s state space and satisfy the safety requirement imposed by software model check.

Key words: Software model check, State-transition model, State explosion, Program conditioning, Theorem proving

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

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

CLC Number: 

• TP311.1