  Verification of concurrent data structures is one of the most challenging
tasks in software verification. The topic has received considerable attention
over the course of the last decade. Nevertheless, human-driven techniques
remain cumbersome and notoriously difficult while automated approaches suffer
from limited applicability. The main obstacle for automation is the complexity
of concurrent data structures. This is particularly true in the absence of
garbage collection. The intricacy of lock-free memory management paired with
the complexity of concurrent data structures makes automated verification
prohibitive.
  In this work we present a method for verifying concurrent data structures and
their memory management separately. We suggest two simpler verification tasks
that imply the correctness of the data structure. The first task establishes an
over-approximation of the reclamation behavior of the memory management. The
second task exploits this over-approximation to verify the data structure
without the need to consider the implementation of the memory management
itself. To make the resulting verification tasks tractable for automated
techniques, we establish a second result. We show that a verification tool
needs to consider only executions where a single memory location is reused. We
implemented our approach and were able to verify linearizability of
Michael&Scott's queue and the DGLM queue for both hazard pointers and
epoch-based reclamation. To the best of our knowledge, we are the first to
verify such implementations fully automatically.
