Skip to main content
SpringerLink
Log in

Completeness for a First-Order Abstract Separation Logic

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10017))

Included in the following conference series:

Abstract

Existing work on theorem proving for the assertion language of separation logic (SL) either focuses on abstract semantics which are not readily available in most applications of program verification, or on concrete models for which completeness is not possible. An important element in concrete SL is the points-to predicate which denotes a singleton heap. SL with the points-to predicate has been shown to be non-recursively enumerable. In this paper, we develop a first-order SL, called FOASL, with an abstracted version of the points-to predicate. We prove that FOASL is sound and complete with respect to an abstract semantics, of which the standard SL semantics is an instance. We also show that some reasoning principles involving the points-to predicate can be approximated as FOASL theories, thus allowing our logic to be used for reasoning about concrete program verification problems. We give some example theories that are sound with respect to different variants of separation logics from the literature, including those that are incompatible with Reynolds’s semantics. In the experiment we demonstrate our FOASL based theorem prover which is able to handle a large fragment of separation logic with heap semantics as well as non-standard semantics.

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 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
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

Notes

  1. 1.

    See http://pl.postech.ac.kr/SL/ for the revised version of their proof system, which is sound but not complete w.r.t. Reynolds’s semantics.

References

  1. Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006). doi:10.1007/11804192_6

    Google Scholar 

  2. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005). doi:10.1007/11575467_5

    Google Scholar 

  3. Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106–137 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  4. Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1–3), 227–270 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  5. Brotherston, J.: A unified display proof theory for bunched logic. ENTCS 265, 197–211 (2010)

    MathSciNet  MATH  Google Scholar 

  6. Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131–146. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22438-6_12

    Chapter  Google Scholar 

  7. Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. J. ACM 61(2), 14:1–14:43 (2014). doi:10.1145/2542667

    Article  MathSciNet  MATH  Google Scholar 

  8. Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: POPL, pp. 453–464. ACM (2014)

    Google Scholar 

  9. Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366–378. IEEE (2007)

    Google Scholar 

  10. Calcagno, C., Yang, H., O’Hearn, P.W.: Computability and Complexity Results for a Spatial Assertion Language for Data Structures. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108–119. Springer, Heidelberg (2001). doi:10.1007/3-540-45294-X_10

    Google Scholar 

  11. Demri, S., Deters, M.: Expressive completeness of separation logic with two variables and no separating conjunction. In: CSL/LICS (2014)

    Google Scholar 

  12. Demri, S., Galmiche, D., Larchey-Wendling, D., Méry, D.: Separation logic with one quantified variable. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.É., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 125–138. Springer, Heidelberg (2014). doi:10.1007/978-3-319-06686-8_10

    Google Scholar 

  13. Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161–177. Springer, Heidelberg (2009). doi:10.1007/978-3-642-10672-9_13

    Chapter  Google Scholar 

  14. Galmiche, D., Méry, D., Pym, D.: The semantics of BI and resource tableaux. MSCS 15(6), 1033–1088 (2005)

    MathSciNet  MATH  Google Scholar 

  15. Galmiche, D., Méry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189–231 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hóu, Z., Clouston, R., Goré, R., Tiu, A.: Proof search for propositional abstract separation logics via labelled sequents. In: POPL (2014)

    Google Scholar 

  17. Hóu, Z., Goré, R., Tiu, A.: Automated theorem proving for assertions in separation logic with all connectives. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 501–516. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21401-6_34

    Chapter  Google Scholar 

  18. Hóu, Z., Tiu, A.: Completeness for a first-order abstract separation logic [cs.LO] (2016). arXiv: 1608.06729

  19. Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 377–396. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28869-2_19

    Chapter  Google Scholar 

  20. Krishnaswami, N.R.: Reasoning about iterators with separation logic. In: SAVCBS, pp. 83–86. ACM (2006)

    Google Scholar 

  21. Larchey-Wendling, D.: The formal strong completeness of partial monoidal Boolean BI. JLC 26(2), 605–640 (2014)

    MathSciNet  MATH  Google Scholar 

  22. Larchey-Wendling, D., Galmiche, D.: Exploring the relation between intuitionistic BI and Boolean BI: an unexpected embedding. MSCS 19(3), 435–500 (2009)

    MathSciNet  MATH  Google Scholar 

  23. Larchey-Wendling, D., Galmiche, D.: The undecidability of Boolean BI through phase semantics. In: LICS, pp. 140–149 (2010)

    Google Scholar 

  24. Larchey-Wendling, D., Galmiche, D.: Looking at separation algebras with Boolean BI-eyes. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 326–340. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44602-7_25

    Google Scholar 

  25. Lee, W., Park, S.: A proof system for separation logic with magic wand. In: POPL, pp. 477–490. ACM (2014)

    Google Scholar 

  26. Maeda, T., Sato, H., Yonezawa, A.: Extended alias type system using separating implication. In: TLDI, pp. 29–42. ACM (2011)

    Google Scholar 

  27. Pérez, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI. ACM (2011)

    Google Scholar 

  28. O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. BSL 5(2), 215–244 (1999)

    MathSciNet  MATH  Google Scholar 

  29. O’Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). doi:10.1007/3-540-44802-0_1

    Google Scholar 

  30. Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL 2013, New York, NY, USA, pp. 219–232 (2013)

    Google Scholar 

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

    Google Scholar 

  32. Schroeder-Heister, Peter: Definitional reflection and the completion. In: Dyckhoff, Roy (ed.) ELP 1993. LNCS, vol. 798, pp. 333–347. Springer, Heidelberg (1994). doi:10.1007/3-540-58025-5_65

    Chapter  Google Scholar 

  33. Thakur, A., Breck, J., Reps, T.: Satisfiability modulo abstraction for separation logic with linked lists. In: SPIN 2014, pp. 58–67 (2014)

    Google Scholar 

  34. Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, New York (1996)

    MATH  Google Scholar 

  35. Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74407-8_18

    Chapter  Google Scholar 

Download references

Acknowledgments

This research is supported by the National Research Foundation, Prime Minister’s Office, Singapore under its National Cybersecurity R&D Program (Award No. NRF2014NCR-NCR001-30) and administered by the National Cybersecurity R&D Directorate.

Author information

Authors and Affiliations

  1. Nanyang Technological University, Singapore, Singapore

    Zhé Hóu & Alwen Tiu

Authors
  1. Zhé Hóu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alwen Tiu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhé Hóu .

Editor information

Editors and Affiliations

  1. Kyoto University , Kyoto, Japan

    Atsushi Igarashi

A An Example Derivation

A An Example Derivation

We sometimes write \(r\times n\) when it is obvious that the rule r is applied n times. We omit some formulae to save space. The derivation is given in the next page. The sub-derivation \(\varPi _1\) is similar to \(\varPi _2\).

figure h

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Hóu, Z., Tiu, A. (2016). Completeness for a First-Order Abstract Separation Logic. In: Igarashi, A. (eds) Programming Languages and Systems. APLAS 2016. Lecture Notes in Computer Science(), vol 10017. Springer, Cham. https://doi.org/10.1007/978-3-319-47958-3_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-47958-3_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-47957-6

  • Online ISBN: 978-3-319-47958-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation