LCS Publication Details
Publication Title: On Our Experience with Modular Pluggable Analyses
Publication Author: Lam, Patrick
Additional Authors: Viktor Kuncak, Martin Rinard
LCS Document Number: MIT-LCS-TR-965
Publication Date: 10-4-2004
LCS Group: Computer Architecture
Additional URL:
Abstract:
We present a technique that enables the focused application of multiple analyses to di erent modules in the same program. In our approach, each module encapsulates one or more data structures and uses membership in abstract sets to characterize how objects participate in data structures. Each analysis veri es that the implementation of the module 1) preserves important internal data structure consistency properties and 2) correctly implements an interface that uses formulas in a set algebra to characterize the e ects of operations on the encapsulated data structures. Collectively, the analyses use the set algebra to 1) characterize how objects participate in multiple data structures and to 2) enable the inter-analysis communication required to verify properties that depend on multiple modules analyzed by different analyses. We have implemented our system and deployed three pluggable analyses into it: a ag analysis for modules in which abstract set membership is determined by a ag eld in each object, a plugin for modules that encapsulate linked data structures such as lists and trees, and an array plugin in which abstract set membership is determined by membership in an array. Our experimental results indicate that our approach makes it possible to e ectively combine multiple analyses to verify properties that involve objects shared by multiple modules, with each analysis analyzing only those modules for which it is appropriate.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.