Modular Verification of Heap Reachability Properties in Separation Logic

Arshavir Ter-Gabrielyan, Alexander J. Summers, Peter Müller

The correctness of many algorithms and data structures depends on reachability properties, that is, on the existence of chains of references between objects in the heap. Reasoning…