Modular Pluggable Analyses for Data Structure Consistency

paper ps   
Hob is a program analysis system that enables the focused application of multiple analyses to different 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 verifies that the implementation of the module 1) preserves important internal data structure consistency properties and 2) correctly implements a set algebra interface that characterizes the effects of operations on the data structure. 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 implemented our system and deployed several pluggable analyses, including a flag analysis for modules in which abstract set membership is determined by a flag field in each object, a PALE shape analysis plugin, and a theorem proving plugin for analyzing arbitrarily complicated data structures. Our experience shows that our system can effectively 1) verify the consistency of data structures encapsulated within a single module and 2) combine analysis results from different analysis plugins to verify properties involving objects shared by multiple modules analyzed by different analyses.

Citation

Viktor Kuncak, Patrick Lam, Karen Zee, and Martin Rinard. Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering (TSE), 32(12), December 2006.

BibTex Entry

@article{KuncakETAL06ModularPluggableAnalysesDataStructureConsistency,
  author = {Viktor Kuncak and Patrick Lam and Karen Zee and Martin Rinard},
  title = {Modular Pluggable Analyses for Data Structure Consistency},
  journal = {IEEE Transactions on Software Engineering (TSE)},
  volume = 32,
  number = 12,
  month = {December},
  year = 2006,
  url = {http://dx.doi.org/10.1109/TSE.2006.125},
  abstract = {
Hob is a program analysis system that enables the
focused application
of multiple analyses to different 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 verifies that the implementation of the module
1) preserves important internal data structure consistency
properties and 2) correctly implements a set algebra interface
that characterizes the effects
of operations on the data structure.
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 implemented our system and deployed several pluggable
analyses, including a flag analysis for modules in which
abstract set membership is determined by a flag field in
each object, a PALE shape analysis plugin, and a theorem
proving plugin for analyzing arbitrarily complicated data
structures.  Our experience shows that our system can
effectively 1) verify the consistency of data structures
encapsulated within a single module and 2) combine analysis
results from different analysis plugins to verify properties
involving objects shared by multiple modules analyzed by
different analyses.
}
}