Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Automated Theory Exploration for Interactive Theorem Proving: Read chapter Read first chapter

2017 | Supplement | Chapter

Proof Tactics for Assertions in Separation Logic

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

Published in: Interactive Theorem Proving

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Efficient, Verified Checking of Propositional Proofs
next chapter Categoricity Results for Second-Order ZF in Dependent Type Theory
Literature
1.
2.
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_​21CrossRef
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_​6CrossRef
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_​5CrossRef
6.
7.
8.
Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. J. ACM 61, 14:1–14:43 (2014)MathSciNetCrossRef
9.
Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: POPL 2014, pp. 453–464 (2014)
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)MathSciNetCrossRef
11.
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007, pp. 366–378. IEEE (2007)
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_​5CrossRef
13.
14.
Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234–245 (2011)
15.
Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ICFP 2009 (2009)
16.
17.
Feng, X.: Local rely-guarantee reasoning. In POPL 2009, pp. 315–327. ACM (2009)
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_​33CrossRefMATH
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)
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_​12CrossRefMATH
21.
Hóu, Z., Clouston, R., Goré, R., Tiu, A.: Proof search for propositional abstract separation logics via labelled sequents. In: POPL 2014 (2014)
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_​34CrossRefMATH
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_​16CrossRefMATH
24.
25.
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_​26CrossRef
27.
Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL 2017, pp. 205–217 (2017)
28.
Lammich, P., Meis, R.: A separation logic framework for imperative HOL. In: AFP 2012 (2012)
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)CrossRef
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
31.
32.
33.
Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL 2013, pp. 219–232 (2013)
34.
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In LICS 2002, pp. 55–74 (2002)
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_​28CrossRefMATH
36.
Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In PLDI 2015, pp. 77–87 (2015)
37.
38.
Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Cambridge Technical report, vol. 687 (2007)
39.
Varming, C., Birkedal, L.: Higher-order separation logic in Isabelle/HOLCF. ENTCS 218, 371–389 (2008)MATH
Metadata
Title
Proof Tactics for Assertions in Separation Logic
Authors
Zhé Hóu
David Sanán
Alwen Tiu
Yang Liu
Copyright Year
2017
Publisher
Springer International Publishing
Book
Interactive Theorem Proving

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

Electronic ISBN: 978-3-319-66107-0

Copyright Year: 2017

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

Premium Partner

    Image Credits