基于反例引导预言的数组理论模下模型检验
计算机科学中的逻辑
2023-06-22 v6
摘要
我们开发了一个通过自动为无限状态系统增广辅助变量来进行模型检验的框架,使得原本需要量化不变式的系统能够进行无量词归纳证明。我们将该机制与针对数组理论的反例引导抽象精化方案相结合。因此,我们的框架在许多情况下可将带量词和数组的归纳推理归约为无量词且无数组的推理。我们在文献中的广泛基准集上评估该方法。结果表明,我们的实现常优于最先进的工具,展示了其实际潜力。
引用
@article{arxiv.2101.06825,
title = {Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays},
author = {Makai Mann and Ahmed Irfan and Alberto Griggio and Oded Padon and Clark Barrett},
journal= {arXiv preprint arXiv:2101.06825},
year = {2023}
}