|
|
Abstract:
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 talk, we present a generalization of Separation Logic which allows to precisely specify complex abstract structures in the heap and the sharing relations among them. Moreover, we introduce 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.
|