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.

翻译：我们开发了一个模型检查无限状态系统的框架,通过自动增加辅助变量,为那些否则需要量化变量的系统提供无量化的上岗证明。我们把这一机制与阵列理论的反指导抽象完善计划结合起来。因此,在许多情况下,我们的框架可以减少与量化和阵列的演导推理,使其与量化和无阵列推理相结合。我们从文献中评估了一套广泛的基准。结果显示,我们的实施往往优于最新工具,显示了其实际潜力。