Name
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 interanalysis 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 plug--in for modules in which abstract set membership is determined by a flag field in each object, a PALE shape analysis plug-in, and a theorem proving plug-in 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 plug-ins to verify properties involving objects shared by multiple modules analyzed by different analyses. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1109/TSE.2006.125 | IEEE Transactions on Software Engineering |
Keywords | Field | DocType |
index terms— typestate,multiple module,modular pluggable analyses,data structure consistency,shape analysis,important internal data structure,pale shape analysis,program verification,different analysis plug-ins,data structure,programming language design,multiple data structure,program analysis,invariant,analysis result,different analysis,formal met hods,complicated data structure,analysis verifies | Data structure,Computer science,Modular design,Database | Journal |
Volume | Issue | ISSN |
32 | 12 | 0098-5589 |
Citations | PageRank | References |
20 | 0.87 | 48 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Viktor Kuncak | 1 | 1129 | 70.57 |
| Patrick Lam | 2 | 636 | 38.73 |
| Karen Zee | 3 | 183 | 8.50 |
| Martin C. Rinard | 4 | 4739 | 277.55 |