一句话：通过自动添加预言变量并结合反例引导抽象精化，将含数组与量词不变式的模型检测归约为无量词、无数组的归纳推理。
无限状态系统的模型检测通常需要带量词的归纳不变式，尤其是涉及数组理论时，归纳推理难以自动化。本文提出一个框架：自动为系统增补辅助（预言，prophecy）变量，使得原本需要量词化不变式的系统能够用无量词的归纳证明完成验证；并将该机制与针对数组理论的反例引导抽象精化（CEGAR）方案相结合。由此，许多情形下带量词与数组的归纳推理被归约为无量词、无数组的推理，从而可交由现成的无量化 SMT 求解器处理。作者在文献中广泛的基准集上评估了实现，结果显示该方法常常优于当前最先进的工具，展示了其实际潜力。
We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.
@article{paperbot1660,
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 = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:26)2022}
}