We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

cs

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

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

Abstract: 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.
Comments: 30 pages, 2 figures, 2 tables, extended version of paper that appeared in International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2021, invited to Logical Methods in Computer Science journal, Version Updates: Notable changes include a self-comparison with different options in Section 7, and Section 6, which discusses implementation details of the prototype
Subjects: Logic in Computer Science (cs.LO)
DOI: 10.1007/978-3-030-72016-2_7
Cite as: arXiv:2101.06825 [cs.LO]
  (or arXiv:2101.06825v3 [cs.LO] for this version)

Submission history

From: Makai Mann [view email]
[v1] Mon, 18 Jan 2021 01:23:00 GMT (254kb,D)
[v2] Wed, 26 May 2021 14:55:21 GMT (269kb,D)
[v3] Wed, 1 Sep 2021 13:41:50 GMT (349kb,D)

Link back to: arXiv, form interface, contact.