We present a numeric analysis that is capable of reasoning about array operations. In particular, the analysis is able to establish that all elements of an array have been initialized (``an array kill''), as well as to discover numeric constraints on values of initialized array elements, and to verify the correctness of comparison-based sorting algorithms. The analysis is based on the combination of canonical abstraction and summarizing numeric domains. We present a prototype implementation of the analysis and discuss our experience with applying this prototype to several kernel examples.

(Click here to access the paper: PDF.)