论文部分内容阅读
提出了一种对并发程序进行切片以缩减模型检验状态空间的方法.首先针对并发程序中的同步与通信定义了一组依赖关系,包括并发分支与接合、非确定性、信道、共享变量等特征.对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准,文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片.可以证明得到的切片与原程序对于该性质具有相同的可满足性.