From Separation Logic to First-Order Logic

Authors

  • Cristiano Calcagno
  • Philippa Gardner
  • Matthew Hague

Abstract

Separation logic is a spatial logic for reasoning locally about heap structures. A decidable fragment of its assertion language was presented in [3], 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 propositional 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.

Venue

Proceedings of the 8th International Conference on Foundations of Software Science and Computational Structures (FOSSACS’05), pp. 395–409

Publication Date

Apr 2005

Identifiers

Source Materials