LARA

Semantics of Dynamic Object Allocation

x = new()

Example program we wish we can prove:

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

Solution:

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.