In this talk I discuss a mechanism for object creation which allows for an optimal use of bounds on the visible heap in model-checking of object-oriented programs.