基于SAT的软件验证

SAT-Based Software Verification

线性时态逻辑SE-LTL是具有高表达力和基于状态、事件推理能力的并发系统规约语言.目前,SE-LTL的模型检测算法依然是显式的,状态空间爆炸是检测的主要困难.对SE-LTL引入一种有界模型检测技术,该技术将SE-LTL模型检测归约为命题公式的可满足性问题,避免了基于二叉图方法中状态空间的快速增长,加速了验证过程.对SE-LTL-X进一步在该技术中集成stuttering等价技术.实验结果表明该集成有效地降低了验证时间.

For concurrent software systems, linear temporal logic SE-LTL is a specification language with high expressive power and the ability to reason about both states and events. Until now, the SE-LTL model checking algorithm is still explicit, and the state explosion is the primary verification difficulty. A bounded model checking procedure is introduced for SE-LTL which reduces model checking to propositional satisfiability. This new technique avoids the space blow up of BDDs, and sometimes speeds up the verification. For SE-LTL-X the procedure and stuttering equivalent technique is further integrated. The experiment result shows that the integration can reduce the verification time very much.