Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures