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

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

Applying Program Conditioning to Reduce State Space for Software Model Checking

Aiming at the state explosion problem existed in the software model checking,a scheme of applying program conditioning to reduce the state space of programs was proposed.Program conditioning consisted of identifying and removing a set of statements which could not be executed when a condition of interest held at some point in a program.In the proposed scheme,the antecedent of an implication form that may apeare in linear temporal logic formula of program properties was taken as the constrained condition of program conditioning;the statements unrelated to the satisfiability of the program properties were deleted with the help of automated theorem prover and through analyzing symbolic execution semantic and reasoning approachability condition.Analysis and experiments show that not only could program conditioning effectively reduce program's state space and relieve the state explosion problem,but also could it produce a reduced model which captured all information relevant to the property being checked and satisfied the safety requirements on state reduction for software model checking.