Leonardo de Moura and Nikolaj Bjorner
4 September 2009
The theory of arrays is ubiquitous in the context of automatic software and hardware verification and symbolic analysis. The basic array theory was introduced by McCarthy and allows to symbolically representing array updates.
To this date the theory of arrays itself remains fundamental to how modern program verification, test-case generation, and model-based program tools model program heaps and higher level data-types, such as sets and finite maps.
We present combinatory array logic, CAL, using a small, but powerful core of combinators, and reduce it to the theory of uninterpreted functions. CAL allows expressing properties that go well beyond the basic array theory. CAL does not allow expressing the identity function I. CAL+I on the other hand allows encoding arbitrary lambda terms. We provide a new efficient decision procedure for the base theory as well as CAL. The efficient procedure serves a critical role in the performance of the state-of-the-art SMT solver Z3 on array formulas from applications.
© 2008 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE. http://www.ieee.org/