基于欠近似精化的谓词抽象

我们提出了一种基于抽象的模型检测方法，该方法依赖于对所分析系统可行行为的欠近似进行精化。由于所有被分析的行为在定义上都是可行的，该方法能够保留对安全性属性的违反（错误）。该方法不需要生成抽象转移关系，而是在存储由一组抽象谓词指定的具体状态的抽象版本的同时，执行具体的转移。对于每个探索的转移，该方法在定理证明器的帮助下检查抽象是否引入了精度损失。这些检查的结果用于决定终止，或通过生成新的抽象谓词来精化抽象。如果所分析的（可能是无限的）具体系统具有有限互模拟商，则该方法保证最终能探索到一个等价的有限互模拟结构。我们展示了该方法在并发程序检测中的应用。