Data Structure Shape Inference and Verification for OO Programs

An approach to static analysis and verification of linked data structures found in OO programs is to firstly infer the ldquoshaperdquo of the object/data structures that may be produced by the program, and secondly to verify that these shapes are consistent with a programmer-specified ldquocorrectrdquo data structure. A feature of the approach is that the shapes of the data structures may be graphed at any time, and are easy to understand. The underlying formalism is presented in abstract interpretation form, and a prototype tool has been developed.