基于内插子的迁移关系近似

在谓词抽象中,精确的像计算是一个难题,最坏情况下需要指数次调用判定过程。因此,软件模型检查器通常使用像的弱近似。这可能导致即使给定了一组充分的谓词,也无法证明某条性质。我们提出一种基于内插子的方法,在出现此类失败时用于强化抽象迁移关系。该方法在给定充分谓词的前提下保证收敛,且无需进行精确的像计算。我们通过实验表明,该方法比早期基于反例分析的方法收敛得更快。