Simulating reachability using first-order logic with applications to verification of linked data structures

Tal Lev-Ami, Neil Immerman, Thomas Reps +3

This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocat…