Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several proposals for the static analysis of programs with arrays, the scalability of these analysis procedures has been an issue. This paper proposes a solution to this problem.

The central contribution of this paper is FunArray, a new abstract domain for arrays. FunArray is actually a functor that can take other abstract domains used for scalar variables and expressions and provide a domain for the arrays. This enables one to choose from the different analysis methods in the scalar variables and expressions, thereby making a tradeoff between precision and speed at the array level.

This abstraction is based on a novel and powerful symbolic representation of arrays as a sequence of consecutive nonoverlapping segments. The strength of this representation stems from the fact that it compactly represents the different cases that one needs to consider while abstracting a concrete array, making the analysis scalable.

The array abstraction is implemented in Clousot, a tool that can automatically generate invariants of programs involving array variables. Clousot has been used to successfully analyze several libraries in .NET that are beyond the reach of other existing techniques.

The authors of this paper are well-known experts in the field. The many examples, as well as the motivating beginning, definitely ease the readability of the paper. The paper is a bit cryptic, though, which is possibly due to size restrictions. An initial reading is likely to pose some difficulties for readers since the presentation contains some unexplained notations, such as “oo” for infinity. Some typographical errors in crucial places further complicate readability. Overall, though, the paper is accessible and useful for researchers working in the area of static analysis.