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

arXiv: https://arxiv.org/abs/2101.06825 · HTML: https://mlsanity.com/paper/2101.06825/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 18 Jan 2021.

## Built on by (most cited first, 2 of 2)

- [Toward Certified Robustness Against Real-World Distribution Shifts](https://mlsanity.com/paper/2206.03669/) (2022)
- [Data-driven Verification of Procedural Programs with Integer Arrays](https://mlsanity.com/paper/2505.15958/) (2025)

## Abstract (arXiv)

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.