Separation logic is a spatial logic for reasoning locally about heap structures. A decidable fragment of its assertion language was presented in [1], based on a bounded model property. We exploit this property to give an encoding of this fragment into a first-order logic containing only the prepositional connectives, quantification over the natural numbers and equality. This result is the first translation from Separation 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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Calcagno, C., Gardner, P., & Hague, M. (2005). From Separation logic to first-order logic. In Lecture Notes in Computer Science (Vol. 3441, pp. 395–409). Springer Verlag. https://doi.org/10.1007/978-3-540-31982-5_25
Mendeley helps you to discover research relevant for your work.