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...

• Type: Conference
• Year: 2005
• Where: VMCAI
• Authors: Patrick Lam, Viktor Kuncak, Martin C. Rinard
• Keywords: Abstract Set Specifications, Abstract Sets, Set Specifications, Software Engineering, VMCAI 2005