| 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.
|