Automating Modular Program Verification by Refining Specifications

Modular analyses of software systems rely on the specifications of the analyzed mod-ules. In many analysis techniques (e.g. ESC/Java), the specifications have to be provided by users. This puts a considerable burden on users and thus limits the applicability of such techniques. To avoid this problem, some modular analysis tech-niques automatically extract module summaries that capture specific aspects of the modules ' behaviors. However, such summaries are only useful in checking a restricted class of properties. We describe a static modular analysis that automatically extracts procedure spec-ifications in order to check heap-manipulating programs against rich data structure properties. Extracted specifications are context-dependent; their precision depends on both the property being checked, and the calling context in which they are used. Starting from a rough over-approximation of the behavior of each call site, our anal-ysis computes an abstraction of the procedure being analyzed and checks it against the property. Specifications are further refined, as needed, in response to spuriou