Sciweavers

VMCAI
2005
Springer

Generalized Typestate Checking for Data Structure Consistency

13 years 9 months ago
Generalized Typestate Checking for Data Structure Consistency
Abstract. We present an analysis to verify abstract set specifications for programs that use object field values to determine the membership of objects in abstract sets. In our approach, each module may encapsulate several data structures membership in abstract sets to characterize how objects participate in its data structures. Each module’s specification uses set algebra formulas to charache effects of its operations on the abstract sets. The program may define set membership in a variety of ways; arbitrary analyses (potentially with multiple analyses applied to different modules in the same program) may verify the corresponding set specifications. The analysis we present in this paper verifies set specifications by constructing and verifying set algebra formulas whose validity implies the validity of the set specifications. We have implemented our analysis and annotated several programs (75-2500 lines of code) with set specifications. We found that our original analysis a...
Patrick Lam, Viktor Kuncak, Martin C. Rinard
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where VMCAI
Authors Patrick Lam, Viktor Kuncak, Martin C. Rinard
Comments (0)