“Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays” by Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, and Clark Barrett. Logical Methods in Computer Science, vol. 18, no. 3, Aug. 2022.
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.
BibTeX entry:
@article{MIG+22,
author = {Makai Mann and Ahmed Irfan and Alberto Griggio and Oded Padon
and Clark Barrett},
title = {Counterexample-Guided Prophecy for Model Checking Modulo the
Theory of Arrays},
journal = {Logical Methods in Computer Science},
volume = {18},
number = {3},
month = aug,
year = {2022},
doi = {10.46298/lmcs-18(3:26)2022},
url = {https://arxiv.org/pdf/2101.06825v6.pdf}
}
(This webpage was created with bibtex2web.)