A Decidable Fragment of Separation Logic

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.

• Type: Conference
• Year: 2004
• Where: FSTTCS
• Authors: Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
• Keywords: Decision Procedure, FSTTCS 2004, Linked List, Study Decision Procedures