A Framework for Numeric Analysis of Array Operations

Automatic discovery of relationships among values of array elements is a challenging problem due to the unbounded nature of arrays. We present a framework for analyzing array operations that is capable of capturing numeric properties of array elements. In particular, the analysis is able to establish that all array elements are initialized by an arrayinitialization loop, as well as to discover numeric constraints on the values of initialized elements