Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

We develop a framework for model checking infinite-state systems byautomatically augmenting them with auxiliary variables, enablingquantifier-free induction proofs for systems that would otherwise requirequantified invariants. We combine this mechanism with a counterexample-guidedabstraction refinement scheme for the theory of arrays. Our framework can thus,in many cases, reduce inductive reasoning with quantifiers and arrays toquantifier-free and array-free reasoning. We evaluate the approach on a wideset of benchmarks from the literature. The results show that our implementationoften outperforms state-of-the-art tools, demonstrating its practicalpotential