Abstract. We present a fragment of separation logic oriented to linked lists, and study decision procedures for validity of entailments. The restrictions in the fragment are motivated by the stylized form of reasoning done in example program proofs. The fragment includes a predicate for describing linked list segments (a kind of reachability or transitive closure). Decidability is first proved by semantic means: by showing a small model property that bounds the size of potential countermodels that must be checked. We then provide a complete proof system for the fragment, the termination of which furnishes a second decision procedure.
A fragment of separation logic for which it is decidable to check validity of entailments was introduced by Berdine et al. REF .
A Decidable Fragment of Separation Logic
FSTTCS
Computer Science