Local reasoning for abstraction and sharing
Renato Cherini, Javier Oscar Blanco · 2009
The local reasoning provided by Separation Logic has been proven to be a good tool for the verification of programs with complex pointer manipulation. However, some problems arise when many structures share part of the heap since it becomes difficult to specify separately and it is even harder to preserve the abstractions that these structures provide. In this article, we present a generalization of Separation Logic which allows us to precisely specify complex abstract structures in the heap and the sharing relations among them. Moreover, we provide also a compositional proof theory which can be used to verify programs in a modular way, even when a complete separation of the structures cannot be ensured.