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

Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh

Browse the full CADE paper archive.