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