A set-theoretic formalism, AOG, is introduced to support automated verification of
pointer programs. AOG targets pointer reasoning for source programs before compilation
(i.e. before removal of field names). Pointer structures are represented as object
graphs instead of heaps. Each property in AOG is a relation between object graphs and
name assignments of program variables, and specifications result from composing 
properties. AOG extends Separation Logic's compositions of address-disjoint separating
conjunction to more restrictive compositions with different disjointness conditions;
the extension is shown to be strict when fixpoints are present. A composition that is
a "unique decomposition" decomposes any given graph uniquely into two parts. An 
example is the separation between the non-garbage and garbage parts of memory. Although
AOG is in general undecidable, it is used to define the semantics of specific decidable
logics that support automated program verification of specific topologies of pointer
structure. One logic studied in this paper describes pointer variables located on 
multiple parallel linked lists. The logic contains quantifiers and fixpoints but is
nonetheless decidable; it is applied to the example of in-place list reversal for
automated verification. The Schorr-Waite marking algorithm is also considered. The
technique of unique decomposition is particularly useful for establishing laws such
logics.