Adapting side effects analysis for modular program model checking

There is a widely held belief that whole program analysis is intractable for large complex software systems, and there can be little doubt that this is true for program analyses based on model checking. Model checking selected program components that comprise a cohesive unit, however, can be an effective way of uncovering subtle coding errors, especially for components of multi-threaded programs. In this setting, one of the chief problems is how to safely approximate the behavior of the rest of the application as it relates to the unit being analyzed.Non-unit application components are collectively referred to as the environment. In this paper, we describe how points-to and side-effects analyses can be adapted to support generation of summaries of environment behavior that can be reified into Java code using special modeling primitives. The resulting abstract models of the environment can be combined with the code of the unit and then model checked against unit properties. We present our analysis framework, illustrate its flexibility in generating several types of models, and present experience that provides evidence of the scalability of the approach.