Extended transitive separation logic ?
A family of stronger separation operators expressing absence of sharing. Hoare-style triples for selector assignments in linked data structures. Use of the logic for reasoning about shape analysis and preservation. Examples: in-situ list reversal, tree rotation, threaded trees, doubly-linked lists.
separation logic sharing reachability strong separation verification