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…