Enforcing Structural Invariants Using Dynamic Frames. - Diego Garbervetsky; Daniel Gorín; Ariel Neisen (TACAS, 2011)