Abstract. We propose a new framework, based on predicate abstraction and model checking, for shape analysis of programs. Shape analysis is used to statically collect information — such as possible reachability and sharing — about program stores. Rather t
31.A.Stump,C.W.Barrett,D.L.Dill,andJ.R.Levitt.Adecisionprocedureforan
extensionaltheoryofarrays.InLICS,pages29–37,2001.
32./~kedar/shape.
33.E.Yahav.VerifyingsafetypropertiesofconcurrentJavaprogramsusing3-valued
logic.InPOPL,pages27–40,2001.