A difficult point when verifying heap manipulating programs is to be able to separate precisely the part of the heap that might be modified by a procedure from the part that will never be touched by that procedure. This is a key point to prove invariants, and in experiments on proving the correctness of design patterns such as the composite pattern, it was indeed pointed as a very consuming task, in term of annotations or guidance of the theorem prover.

In this talk, we will show that it is possible to infer automatically such modification shapes in the context of abstract interpretation with shape graphs.

This is joint work with Anindya Banerjee.