This work was carried out under the supervision of

Shape analysis algorithms conservatively verify imperative programs and algorithms that use destructive pointer updates to manipulate dynamically allocated linked data structures. One of the challenges in developing such shape analyses is the computation of abstract transformers, i.e., the effect of program statements on the abstract representation of the memory. In this the-sis, we explore three different approaches for computing these abstract transformers. Special emphasis is given to harnessing existing tools and analyses and adapting them to perform richer analyses. We start by exploring the use of first order automated theorem provers. These powerful tools have advanced considerably in the last decade and are able to deal with complex reason-ing problems. The main obstacle in using these tools is that reasoning about data structures requires an understanding of reachability within the program heap, which cannot be expressed in first order logic. We overcome this obstacle by developing a partial axiomatization of tran-sitive closure, which allows us to express reachability. The axiomatization is mechanizable and allows automatically proving properties both using hand written invariants and by infer