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.

PDF file

In: FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings

Publisher: Springer

Details