针对安全性质的归纳有效性核的高效生成

符号模型检测器能够为非常复杂的模型构造性质证明。然而，当证明成功时，工具报告的结果通常不能为用户提供太多洞察。用户拥有与证明相关的可追溯性信息往往很有用：即模型的哪些部分对于构造该证明是必要的。这种可追溯性信息可用于诊断多种建模问题，例如过度约束的公理与约束不足的性质，也可用于度量模型上需求集的完备性。在本文中，我们提出一种新算法，用于高效计算时序系统安全性质归纳证明所必需的模型内归纳有效性核（IVC）。该算法基于当前 SMT 求解器内置的 UNSAT 核支持，以及对归纳问题的一种新颖编码，试图生成极小的归纳有效性核。我们证明了算法的正确性，并描述了其在面向 Lustre 模型的 JKind 模型检测器中的实现。随后我们给出一个实验，从速度、所生成核的多样性以及极小性方面对该算法进行基准测试，取得了有前景的结果。