Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Automated Theory Exploration for Interactive Theorem Proving: Kapitel lesen Erstes Kapitel lesen

2017 | Supplement | Buchkapitel

Proof Tactics for Assertions in Separation Logic

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

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Vorheriges Kapitel Efficient, Verified Checking of Propositional Proofs
Nächstes Kapitel Categoricity Results for Second-Order ZF in Dependent Type Theory
Literatur
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.
Brotherston, J.: A unified display proof theory for bunched logic. ENTCS 265, 197–211 (2010)MathSciNetMATH
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
Metadaten
Titel
Proof Tactics for Assertions in Separation Logic
verfasst von
Zhé Hóu
David Sanán
Alwen Tiu
Yang Liu
Copyright-Jahr
2017
Verlag
Springer International Publishing
Buch
Interactive Theorem Proving

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

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

Copyright-Jahr: 2017

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

Premium Partner

    Bildnachweise