From separation logic to first-order logic

Abstract

Separation logic is a spatial logic for reasoning locally about heap structures. A decidable fragment of its assertion language was pre- sented in [1], based on a bounded model property. We exploit this prop- erty to give an encoding of this fragment into a first-order logic contain- ing only the propositional connectives, quantification over the natural numbers and equality. This result is the first translation from Separa- tion Logic into a logic which does not depend on the heap, and provides a direct decision procedure based on well-studied algorithms for first- order logic. Moreover, our translation is compositional in the structure of formulae, whilst previous results involved enumerating either heaps or formulae arising from the bounded model property.