On Modular Pluggable Analyses Using Set Interfaces
We present a technique that enables the focused applicationof multiple analyses to different modules in the same program. Our researchhas two goals: 1) to address the scalability limitations of preciseanalyses by focusing the analysis on only those parts of the program thatare relevant to the proper...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2005
|
| Online Access: | http://hdl.handle.net/1721.1/30441 |
| _version_ | 1824457819606220800 |
|---|---|
| author | Lam, Patrick Kuncak, Viktor Rinard, Martin |
| author2 | Computer Architecture |
| author_facet | Computer Architecture Lam, Patrick Kuncak, Viktor Rinard, Martin |
| author_sort | Lam, Patrick |
| collection | MIT |
| description | We present a technique that enables the focused applicationof multiple analyses to different modules in the same program. Our researchhas two goals: 1) to address the scalability limitations of preciseanalyses by focusing the analysis on only those parts of the program thatare relevant to the properties that the analysis is designed to verify, and2) to enable the application of specialized analyses that verify propertiesof specifc classes of data structures to programs that simultaneouslymanipulate several dfferent kinds of data structures.In our approach, each module encapsulates a data structure and usesmembership in abstract sets to characterize how objects participate inits data structure. Each analysis verifies that the implementation of themodule 1) preserves important internal data structure representationinvariants and 2) conforms to a specification that uses formulas in a setalgebra to characterize the effects of operations on the data structure.The analyses use the common set abstraction to 1) characterize howobjects participate in multiple data structures and to 2) enable the interanalysiscommunication required to verify properties that depend onmultiple modules analyzed by different analyses.We characterize the key soundness property that an analysis plugin mustsatisfy to successfully participate in our system and present several analysisplugins that satisfy this property: a flag plugin that analyzes modulesin which abstract set membership is determined by a flag field in eachobject, and a graph types plugin that analyzes modules in which abstractset membership is determined by reachability properties of objects storedin tree-like data structures. |
| first_indexed | 2024-09-23T08:45:18Z |
| id | mit-1721.1/30441 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T08:45:18Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/304412019-04-10T07:19:15Z On Modular Pluggable Analyses Using Set Interfaces Lam, Patrick Kuncak, Viktor Rinard, Martin Computer Architecture We present a technique that enables the focused applicationof multiple analyses to different modules in the same program. Our researchhas two goals: 1) to address the scalability limitations of preciseanalyses by focusing the analysis on only those parts of the program thatare relevant to the properties that the analysis is designed to verify, and2) to enable the application of specialized analyses that verify propertiesof specifc classes of data structures to programs that simultaneouslymanipulate several dfferent kinds of data structures.In our approach, each module encapsulates a data structure and usesmembership in abstract sets to characterize how objects participate inits data structure. Each analysis verifies that the implementation of themodule 1) preserves important internal data structure representationinvariants and 2) conforms to a specification that uses formulas in a setalgebra to characterize the effects of operations on the data structure.The analyses use the common set abstraction to 1) characterize howobjects participate in multiple data structures and to 2) enable the interanalysiscommunication required to verify properties that depend onmultiple modules analyzed by different analyses.We characterize the key soundness property that an analysis plugin mustsatisfy to successfully participate in our system and present several analysisplugins that satisfy this property: a flag plugin that analyzes modulesin which abstract set membership is determined by a flag field in eachobject, and a graph types plugin that analyzes modules in which abstractset membership is determined by reachability properties of objects storedin tree-like data structures. 2005-12-22T01:15:47Z 2005-12-22T01:15:47Z 2003-12-18 MIT-CSAIL-TR-2003-036 MIT-LCS-TR-933 http://hdl.handle.net/1721.1/30441 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 34 p. 31854752 bytes 1275133 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Lam, Patrick Kuncak, Viktor Rinard, Martin On Modular Pluggable Analyses Using Set Interfaces |
| title | On Modular Pluggable Analyses Using Set Interfaces |
| title_full | On Modular Pluggable Analyses Using Set Interfaces |
| title_fullStr | On Modular Pluggable Analyses Using Set Interfaces |
| title_full_unstemmed | On Modular Pluggable Analyses Using Set Interfaces |
| title_short | On Modular Pluggable Analyses Using Set Interfaces |
| title_sort | on modular pluggable analyses using set interfaces |
| url | http://hdl.handle.net/1721.1/30441 |
| work_keys_str_mv | AT lampatrick onmodularpluggableanalysesusingsetinterfaces AT kuncakviktor onmodularpluggableanalysesusingsetinterfaces AT rinardmartin onmodularpluggableanalysesusingsetinterfaces |