Automatic inference of invariants in objects with variable structure

This paper considers automatic inference of invariants in objects with variable structure. We say for an object that it has variable structure if a part of its logical memory space is on the heap and is linked with the host with a reference (pointer). We infer the strong invariant for the linked list, provided that our approach is applicable to all container classes.