基于反例引导的数组理论模型检查的预测
摘要：无穷状态系统的模型检验框架的发展通过自动为其附加辅助变量来实现，使得对于否则需要量化不变性的系统可以进行无量词归纳证明。我们将这种机制与针对数组理论的反例引导抽象精炼方案相结合。因此，我们的框架在许多情况下可以将带有量词和数组的归纳推理简化为无量词和无数组的推理。我们在文献中的广泛基准测试集上评估了这种方法。结果表明，我们的实现经常胜过最先进的工具，展示了其实际潜力。
作者：Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, Clark Barrett
论文ID：2101.06825
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22