Skip to main content
SpringerLink
Log in

Transitive Separation Logic

  • Conference paper
Relational and Algebraic Methods in Computer Science (RAMICS 2012)

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

Abstract

Separation logic (SL) is an extension of Hoare logic by operations and formulas that not only talk about program variables, but also about heap portions. Its general purpose is to enable more flexible reasoning about linked object/record structures. In the present paper we give an algebraic extension of SL at the data structure level. We define operations that additionally to heap separation make assumptions about the linking structure. Phenomena to be treated comprise reachability analysis, (absence of) sharing, cycle detection and preservation of substructures under destructive assignments. We demonstrate the practicality of this approach with the examples of in-place list-reversal and tree rotation.

An Erratum for this chapter can be found at http://dx.doi.org/10.1007/978-3-642-33314-9_24

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Berdine, J., Calcagno, C., O’Hearn, P.W.: A Decidable Fragment of Separation Logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 97–109. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  2. Calcagno, C., O’Hearn, P.W., Yang, H.: Local Action and Abstract Separation Logic. In: Proc. of the 22nd Symposium on Logic in Computer Science, pp. 366–378. IEEE Press (2007)

    Google Scholar 

  3. Chen, Y., Sanders, J.W.: Abstraction of Object Graphs in Program Verification. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 80–99. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Dang, H.H., Höfner, P., Möller, B.: Algebraic separation logic. Journal of Logic and Algebraic Programming 80(6), 221–247 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  5. Desharnais, J., Möller, B.: Characterizing determinacy in Kleene algebra. Information Sciences 139, 253–273 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  6. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Transactions on Computational Logic 7(4), 798–833 (2006)

    Article  MathSciNet  Google Scholar 

  7. Ehm, T.: The Kleene algebra of nested pointer structures: Theory and applications, PhD Thesis (2003), http://www.opus-bayern.de/uni-augsburg/frontdoor.php?source_opus=89

  8. Ehm, T.: Pointer Kleene Algebra. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS/Kleene-Algebra Ws 2003. LNCS, vol. 3051, pp. 99–111. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Hoare, C.A.R.: Proofs of correctness of data representations. Acta Informatica 1, 271–281 (1972)

    Article  MATH  Google Scholar 

  10. Hoare, C.A.R., Hussain, A., Möller, B., O’Hearn, P.W., Petersen, R.L., Struth, G.: On Locality and the Exchange Law for Concurrent Processes. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 250–264. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Höfner, P., Struth, G.: Can refinement be automated? In: Boiten, E., Derrick, J., Smith, G. (eds.) Refine 2007. ENTCS, vol. 201, pp. 197–222. Elsevier (2008)

    Google Scholar 

  12. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  13. Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19(3), 427–443 (1997)

    Article  MATH  Google Scholar 

  14. Manes, E., Benson, D.: The inverse semigroup of a sum-ordered semiring. Semigroup Forum 31, 129–152 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  15. McCune, W.W.: Prover9 and Mace4, http://www.cs.unm.edu/~mccune/prover9

  16. Möller, B.: Some applications of pointer algebra. In: Broy, M. (ed.) Programming and Mathematical Method. NATO ASI Series, Series F: Computer and Systems Sciences, vol. 88, pp. 123–155. Springer (1992)

    Google Scholar 

  17. Möller, B.: Calculating with acyclic and cyclic lists. Information Sciences 119(3-4), 135–154 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  18. O’Hearn, P.W.: Resources, Concurrency, and Local Reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  19. Reynolds, J.C.: An introduction to separation logic. In: Broy, M. (ed.) Engineering Methods and Tools for Software Safety and Security, pp. 285–310. IOS Press (2009)

    Google Scholar 

  20. Sims, E.J.: Extending Separation Logic with Fixpoints and Postponed Substitution. Theoretical Computer Science 351(2), 258–275 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  21. Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. Journal of Automated Reasoning 21(2), 177–203 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  22. Wang, S., Barbosa, L.S., Oliveira, J.N.: A Relational Model for Confined Separation Logic. In: Proc. of the 2nd IFIP/IEEE Intl. Symposium on Theoretical Aspects of Software Engineering, TASE 2008, pp. 263–270. IEEE Press (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Universität Augsburg, D-86159, Augsburg, Germany

    Han-Hing Dang & Bernhard Möller

Authors
  1. Han-Hing Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing and Software, McMaster University, 1280 Main Street West, L8S 4K1, Hamilton, ON, Canada

    Wolfram Kahl

  2. Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, CB3 0FD, Cambridge, UK

    Timothy G. Griffin

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dang, HH., Möller, B. (2012). Transitive Separation Logic. In: Kahl, W., Griffin, T.G. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2012. Lecture Notes in Computer Science, vol 7560. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33314-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33314-9_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33313-2

  • Online ISBN: 978-3-642-33314-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation