Skip to main content
SpringerLink
Log in

Proof Tactics for Assertions in Separation Logic

  • Conference paper
Book cover Interactive Theorem Proving (ITP 2017)

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

Included in the following conference series:

Abstract

This paper presents tactics for reasoning about the assertions of separation logic. We formalise our proof methods in Isabelle/HOL based on Klein et al.’s separation algebra library. Our methods can also be used in other separation logic frameworks that are instances of the separation algebra of Calcagno et al. The first method, \( separata \), is based on an embedding of a labelled sequent calculus for abstract separation logic (ASL) by Hóu et al. The second method, \( starforce \), is a refinement of separata with specialised proof search strategies to deal with separating conjunction and magic wand. We also extend our tactics to handle pointers in the heap model, giving a third method \( sepointer \). Our tactics can automatically prove many complex formulae. Finally, we give two case studies on the application of our tactics.

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

References

  1. Facebook Infer. http://fbinfer.com/

  2. Isabelle/HOL tactics for separation algebra. http://securify.scse.ntu.edu.sg/SoftVer/Separata

  3. Bengtson, J., Jensen, J.B., Birkedal, L.: Charge! a framework for higher-order separation logic in Coq. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 315–331. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32347-8_21

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  6. Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 323–338. Springer, Heidelberg (2008). doi:10.1007/978-3-540-87531-4_24

    Chapter  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  8. Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. J. ACM 61, 14:1–14:43 (2014)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  10. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 1–66 (2011)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  12. Cervesato, I., Hodas, J.S., Pfenning, F.: Efficient resource management for linear logic proof search. In: Dyckhoff, R., Herre, H., Schroeder-Heister, P. (eds.) ELP 1996. LNCS, vol. 1050, pp. 67–81. Springer, Heidelberg (1996). doi:10.1007/3-540-60983-0_5

    Chapter  Google Scholar 

  13. Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 200–215. Springer, Heidelberg (2005). doi:10.1007/11538363_15

    Chapter  MATH  Google Scholar 

  14. Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234–245 (2011)

    Google Scholar 

  15. Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ICFP 2009 (2009)

    Google Scholar 

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

  17. Feng, X.: Local rely-guarantee reasoning. In POPL 2009, pp. 315–327. ACM (2009)

    Google Scholar 

  18. Galmiche, D., Larchey-Wendling, D.: Expressivity properties of Boolean BI through relational models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 357–368. Springer, Heidelberg (2006). doi:10.1007/11944836_33

    Chapter  MATH  Google Scholar 

  19. Ronghui, G., Shao, Z., Chen, H., Xiongnan, W., Kim, J., Sjöberg, V., Costanzo, D.: Certikos: an extensible architecture for building certified concurrent OS kernels. In OSDI 2016, pp. 653–669 (2016)

    Google Scholar 

  20. Hodas, J.S., López, P., Polakow, J., Stoilova, L., Pimentel, E.: A tag-frame system of resource management for proof search in linear-logic programming. In: Bradfield, J. (ed.) CSL 2002. LNCS, vol. 2471, pp. 167–182. Springer, Heidelberg (2002). doi:10.1007/3-540-45793-3_12

    Chapter  MATH  Google Scholar 

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

    Google Scholar 

  22. 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, Cham (2015). doi:10.1007/978-3-319-21401-6_34

    Chapter  MATH  Google Scholar 

  23. Hóu, Z., Tiu, A., Goré, R.: A labelled sequent calculus for BBI: proof theory and proof search. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS, vol. 8123, pp. 172–187. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40537-2_16

    Chapter  MATH  Google Scholar 

  24. Hóu, Z., Tiu, A.: Completeness for a first-order abstract separation logic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 444–463. Springer, Cham (2016). doi:10.1007/978-3-319-47958-3_23

    Chapter  Google Scholar 

  25. Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332–337. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32347-8_22

    Chapter  Google Scholar 

  26. Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696–723. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54434-1_26

    Chapter  Google Scholar 

  27. Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL 2017, pp. 205–217 (2017)

    Google Scholar 

  28. Lammich, P., Meis, R.: A separation logic framework for imperative HOL. In: AFP 2012 (2012)

    Google Scholar 

  29. Larchey-Wendling, D., Galmiche, D.: Non-deterministic phase semantics and the undecidability of Boolean BI. ACM TOCL 14(1), 6:1–6:41 (2013)

    Article  Google Scholar 

  30. Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: SP 2013, pp. 415–429, May 2013

    Google Scholar 

  31. Myreen, M.O.: Separation logic adapted for proofs by rewriting. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 485–489. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14052-5_34

    Chapter  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  33. Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL 2013, pp. 219–232 (2013)

    Google Scholar 

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

    Google Scholar 

  35. Sanán, D., Zhao, Y., Hou, Z., Zhang, F., Tiu, A., Liu, Y.: CSimpl: a rely-guarantee-based framework for verifying concurrent programs. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 481–498. Springer, Heidelberg (2017). doi:10.1007/978-3-662-54577-5_28

    Chapter  MATH  Google Scholar 

  36. Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In PLDI 2015, pp. 77–87 (2015)

    Google Scholar 

  37. Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469–484. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_32

    Chapter  MATH  Google Scholar 

  38. Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Cambridge Technical report, vol. 687 (2007)

    Google Scholar 

  39. Varming, C., Birkedal, L.: Higher-order separation logic in Isabelle/HOLCF. ENTCS 218, 371–389 (2008)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Nanyang Technological University, Singapore, Singapore

    Zhé Hóu, David Sanán, Alwen Tiu & Yang Liu

Authors
  1. Zhé Hóu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Sanán
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alwen Tiu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yang Liu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Brasília, Brasília D.F., Brazil

    Mauricio Ayala-Rincón

  2. NASA, Hampton, VA, USA

    César A. Muñoz

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Hóu, Z., Sanán, D., Tiu, A., Liu, Y. (2017). Proof Tactics for Assertions in Separation Logic. In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66107-0_19

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66106-3

  • Online ISBN: 978-3-319-66107-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation