hought of as abstract interpretation for the heap How we talk about the heap Program var X points to U that has an N field pointing to V We use first order predicate logic ¡ Description is called a logical structure ¡ Heap objects are the logical variables ¡ Predicates represent program variables X U N V X(U) = 1, X(V) = 0 N(U,V) = 1, N(V,U) = 0, N(U,U) = 0, N(V,V) = 0 Structure S
Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm