一种基于满足性判定的并发软件验证策略

对线性时态逻辑se-ltl提出了一种基于sat的有界模型检测过程,该过程避免了基于bdd方法中状态空间快速增长的问题.在se-ltl的子集se-ltl?x的有界模型检测过程中,集成了stuttering等价技术,该集成有效地加速了验证过程.进一步提出了一种组合了基于sat的有界模型检测、基于反例的抽象求精、组合推理3种状态空间约简技术的并发软件验证策略.该策略中,抽象和求精在每一个构件上独立进行.同时,模型检测的过程是符号化的.实例表明,该策略降低了验证时间和对内存空间的需求.