33 citations · 55 across the 3 of their papers we have counts for
3 papers
cs.LO2009★ 8 cited
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…
cs.LO2007★ 33 cited
A Logic of Reachable Patterns in Linked Data-Structures
Greta Yorsh, Alexander Rabinovich, Mooly Sagiv +2
We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The m…
cs.LO2003★ 14 cited
Logical Characterizations of Heap Abstractions
G. Yorsh, T. Reps, M. Sagiv +1
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown…