Simulating reachability using first-order logic with applications to verification of linked data structures (Logical Methods in Computer Science, 2009)