A Framework for Numeric Analysis of Array Operations
D. Gopan, T. Reps, and M. Sagiv
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
array-initialization loop, as well as to discover numeric constraints on
the values of initialized elements.
The analysis is based on the combination of canonical abstraction and
summarizing numeric domains. We describe a prototype implementation of
the analysis and discuss our experience with applying the prototype to
several examples, including the verification of correctness of an
insertion-sort procedure.
(Click here to access the paper:
PostScript,
PDF.)