||On Modular Pluggable Analyses Using Set Interfaces
||Viktor Kuncak, Martin Rinard
|LCS Document Number:
|We present a technique that enables the focused application
of multiple analyses to different modules in the same program. Our research
has two goals: 1) to address the scalability limitations of precise
analyses by focusing the analysis on only those parts of the program that
are relevant to the properties that the analysis is designed to verify, and
2) to enable the application of specialized analyses that verify properties
of specifc classes of data structures to programs that simultaneously
manipulate several dfferent kinds of data structures.
In our approach, each module encapsulates a data structure and uses
membership in abstract sets to characterize how objects participate in
its data structure. Each analysis verifies that the implementation of the
module 1) preserves important internal data structure representation
invariants and 2) conforms to a specification that uses formulas in a set
algebra to characterize the effects of operations on the data structure.
The analyses use the common set abstraction to 1) characterize how
objects participate in multiple data structures and to 2) enable the interanalysis
communication required to verify properties that depend on
multiple modules analyzed by different analyses.
We characterize the key soundness property that an analysis plugin must
satisfy to successfully participate in our system and present several analysis
plugins that satisfy this property: a
flag plugin that analyzes modules
in which abstract set membership is determined by a
flag field in each
object, and a graph types plugin that analyzes modules in which abstract
set membership is determined by reachability properties of objects stored
in tree-like data structures.
|To obtain this publication:
To purchase a printed copy of this publication please contact