Skip to main content
SpringerLink
Log in

On the Almighty Wand

  • Conference paper
Computer Science Logic (CSL 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5213))

Included in the following conference series:

Abstract

We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL) and its fragments. SL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as SL and as a by-product we get undecidability of SL. This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. As a consequence of this deep result, in SL the magic wand can simulate the separating conjunction. By contrast, we establish that SL without the magic wand is decidable with non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. Equivalence between second-order logic and separation logic extends to the case with more than one selector.

Supported by RNTL project AVERILES - R. Brochenin is supported by a DGA/CNRS fellowship.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 109.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 139.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. Brochenin, R., Demri, S., Lozes, E.: Reasoning about sequences of memory states. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 100–114. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Technical report, LSV, ENS de Cachan (2008)

    Google Scholar 

  4. Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  5. Bouajjani, A., Habermehl, P., Moro, P., Vojnar, T.: Verifying programs with dynamic 1-selector-linked structured in regular model-checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 13–29. Springer, Heidelberg (2005)

    Google Scholar 

  6. Bozga, M., Iosif, R., Lakhnech, Y.: On logics of aliasing. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 344–360. Springer, Heidelberg (2004)

    Google Scholar 

  7. Bozga, M., Iosif, R., Perarnau, S.: Quantitative separation logic and programs with lists. In: IJCAR 2008 (to appear, 2008)

    Google Scholar 

  8. Calcagno, C., Gardner, P., Hague, M.: From separation logic to first-order logic. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 395–409. Springer, Heidelberg (2005)

    Google Scholar 

  9. Calcagno, C., Yang, H., O’Hearn, P.: Computability and complexity results for a spatial assertion language. In: APLAS 2001, pp. 289–300 (2001)

    Google Scholar 

  10. Calcagno, C., Yang, H., O’Hearn, P.: 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)

    Chapter  Google Scholar 

  11. Dawar, A., Gardner, P., Ghelli, G.: Adjunct elimination through games in static ambient logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 211–223. Springer, Heidelberg (2004)

    Google Scholar 

  12. Dawar, A., Gardner, P., Ghelli, G.: Expressiveness and complexity of graph logic. I & C 205(3), 263–310 (2007)

    MATH  MathSciNet  Google Scholar 

  13. Galmiche, D., Méry, D.: Tableaux and resource graphs for separation logic (submitted, 2008)

    Google Scholar 

  14. Ishtiaq, S., O’Hearn, P.: BI as an assertion language for mutable data structures. In: POPL 2001, pp. 14–26 (2001)

    Google Scholar 

  15. Jensen, J., Jorgensen, M., Klarlund, N., Schwartzbach, M.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI 1997, pp. 226–236. ACM, New York (1997)

    Chapter  Google Scholar 

  16. Klaedtke, F., Rueb, H.: Monadic second-order logics with cardinalities. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 681–696. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Kuncak, V., Rinard, M.: On spatial conjunction as second-order logic. Technical report, MIT CSAIL (October 2004)

    Google Scholar 

  18. Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–302. Springer, Heidelberg (2000)

    Google Scholar 

  19. Lozes, E.: Separation logic preserves the expressive power of classical logic. In: 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE 2004) (2004)

    Google Scholar 

  20. Lozes, E.: Elimination of spatial connectives in static spatial logics. TCS 330(3), 475–499 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  21. Löding, C., Rohde, P.: Model checking and satisfiability for sabotage modal logic. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 302–313. Springer, Heidelberg (2003)

    Google Scholar 

  22. Marcinkowski, J.: On the expressive power of graph logic. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 486–500. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Magill, S., Berdine, J., Clarke, E., Cook, B.: Arithmetic strengthening for shape analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 419–436. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  24. Rabin, M.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 41, 1–35 (1969)

    Article  MathSciNet  Google Scholar 

  25. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE, Los Alamitos (2002)

    Google Scholar 

  26. Ranise, S., Zarba, C.: A theory of singly-linked lists and its extensible decision procedure. In: SEFM 2006, pp. 206–215. IEEE, Los Alamitos (2006)

    Google Scholar 

  27. Stockmeyer, L.: The complexity of decision problems in automata theory and logic. PhD thesis, Department of Electrical Engineering. MIT (1974)

    Google Scholar 

  28. Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem for finite models. Dokl. Akad. Nauk SSSR 70, 566–572 (1950); English translation in: AMS Transl. Ser. 2, 23(1063), 1–6

    Google Scholar 

  29. Yorsh, G., Rabinovich, A.M., Sagiv, M., Meyer, A., Bouajjani, A.: A logic of reachable patterns in linked data structures. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 94–110. Springer, Heidelberg (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan, CNRS, INRIA Saclay, France

    Rémi Brochenin, Stéphane Demri & Etienne Lozes

Authors
  1. Rémi Brochenin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stéphane Demri
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Etienne Lozes
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michael Kaminski Simone Martini

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Brochenin, R., Demri, S., Lozes, E. (2008). On the Almighty Wand. In: Kaminski, M., Martini, S. (eds) Computer Science Logic. CSL 2008. Lecture Notes in Computer Science, vol 5213. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-87531-4_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-87531-4_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-87530-7

  • Online ISBN: 978-3-540-87531-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation