x = new()

Example program we wish we can prove:

 x = new();
 y = new();
 assert (x != y);

Solution:

x = new();

assume (x1 notin S);
x = x1;
S = S U {x1};

What should we assume about references to and from allocated objects?

We obtain formulas with sets, in FOL eliminate them using quantifiers as in Deciding a language of sets and relations.