Abstract
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 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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE, Los Alamitos (2002)
Berdine, J., Calcagno, C., O’Hearn, P.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004)
Zilio, S.D., Lugiez, D., Meyssonnier, C.: A logic you can count on. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 135–146. ACM Press, New York (2004)
Cardelli, L., Gordon, A.D.: Anytime, anywhere: Modal logics for mobile ambients. In: 27th Symposium on Principles of Programming Languages (POPL 2000), pp. 365–377. ACM, New York (2000)
Lozes, E.: Separation logic preserves the expressive power of classical logic. As published at (2004), http://www.diku.dk/topps/space2004/space_final/etienne.pdf
Lozes, E.: Elimination of spatial connectives in static spatial logics. To Appear in TCS (2004)
Hague, M.: Static checkers for tree structures and heaps. Master’s thesis, Imperial College London, Department of Computing (2004), http://www.doc.ic.ac.uk/~ajf/Teaching/Projects/Distinguished04/MatthewHague.pdf
Cardelli, L., Caires, L.: A spatial logic for concurrency (part I). Journal of Information and Computation 186(2) (2003)
Cardelli, L., Caires, L.: A spatial logic for concurrency (part II). To Appear in Theoretical Computer Science (2004)
Cardelli, L., Gardner, P., Ghelli, G.: A spatial logic for querying graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, p. 597. Springer, Heidelberg (2002)
Cardelli, L., Gardner, P., Ghelli., G.: Querying trees with pointers. Unpublished Notes, 2003; talk at APPSEM 2001 (2003)
Calcagno, C., Gardner, P., Zarfaty, U.: Context logic and tree update. To appear in POPL (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Calcagno, C., Gardner, P., Hague, M. (2005). From Separation Logic to First-Order Logic. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)