Weakly Equivalent Arrays
Logic in Computer Science
2014-05-28 v1
Abstract
The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. Current decision procedures for the theory of arrays saturate the read-over-write and extensionality axioms originally proposed by McCarthy. Various filters are used to limit the number of axiom instantiations while preserving completeness. We present an algorithm that lazily instantiates lemmas based on weak equivalence classes. These lemmas are easier to interpolate as they only contain existing terms. We formally define weak equivalence and show correctness of the resulting decision procedure.
Cite
@article{arxiv.1405.6939,
title = {Weakly Equivalent Arrays},
author = {Jürgen Christ and Jochen Hoenicke},
journal= {arXiv preprint arXiv:1405.6939},
year = {2014}
}