Ieee Transactions on Software Engineering 1 Modular Pluggable Analyses for Data Structure Consistency
Ieee Transactions on Software Engineering 1 Modular Pluggable Analyses for Data Structure Consistency
复制标题
IEEE Transactions on Software Engineering 1 数据结构一致性的模块化可插入分析
DOI：
--
复制
发表时间：
--
期刊：
影响因子：
--
通讯作者：
M. Rinard
中科院分区：
文献类型：
--
作者：
Viktor Kunčak;Patrick Lam;Karen Zee;M. Rinard
- Hob是一个程序分析系统，它可以将多个分析集中应用于同一程序中的不同模块。在我们的方法中，每个模块封装一个或多个数据结构，并使用抽象集合中的成员资格来表征对象如何参与数据结构。每个分析都验证了模块的实现：1）保留了重要的内部数据结构一致性属性; 2）正确地实现了一个集合代数接口，该接口表征了操作对数据结构的影响。总的来说，分析使用集合代数来1）表征对象如何参与多个数据结构，以及2）实现验证依赖于由不同分析分析的多个模块的属性所需的分析间通信。我们实现了我们的系统，并部署了几个可插拔的分析，包括一个标志分析模块，其中抽象的集合成员是由每个对象中的标志字段，一个PALE形状分析插件，和一个定理证明插件分析任意复杂的数据结构。我们的经验表明，我们的系统可以有效地1）验证封装在一个单一的模块和2）联合收割机的分析结果，从不同的分析插件，以验证属性，涉及对象共享的多个模块分析不同的分析的数据结构的一致性。
— 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.
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds