The finite-state model checking of software is still limited by the notorious state-explosion problem. The dependence-based program slicing is effective to reduce the verification time and is orthogonal to other reduction techniques of model checking. However, within slicing concurrent programs for model checking, the conversions between multiple irreplaceable models and the calculation of dependencies for some variables irrelevant to the verified property produce redundant calculating costs. Thus, we propose a Program Dependence Net (PDNet) as a unified model combining the control-flow structure with dependencies to avoid the model conversions. For reduction, we propose a PDNet slicing to capture the relevant variables' dependencies on demand. The calculating costs could be significantly compressed by our unified model and on-demand slicing based on PDNet. Then, we implemented a concurrent program model checking tool based on PDNet and its slice. Finally, we validated the advantages of our methods.

翻译：软件的有穷状态模型检测仍受制于著名的状态爆炸问题。基于依赖的程序切片能有效降低验证时间，并且与模型检测的其他约简技术正交。然而，在对并发程序进行面向模型检测的切片时，多个不可替代模型之间的转换以及某些与验证性质无关的变量的依赖计算会产生冗余的计算开销。为此，我们提出程序依赖网（Program Dependence Net, PDNet）作为统一模型，将控制流结构与依赖关系相结合，以避免模型转换。为进行约简，我们提出PDNet切片，按需捕获相关变量的依赖关系。通过统一模型和基于PDNet的按需切片，计算开销可显著压缩。随后，我们基于PDNet及其切片实现了一个并发程序模型检测工具。最后，我们验证了所提方法的优势。