nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Completeness for a First-Order Abstract Separation Logic

verfasst von : Zhé Hóu, Alwen Tiu

Erschienen in: Programming Languages and Systems

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

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.

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 Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic

Nur mit Berechtigung zugänglich

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.

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

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

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

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

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

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 CrossRef

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 MathSciNetCrossRefMATH

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

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

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

11.

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

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

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 CrossRef

14.

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

15.

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

16.

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

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 CrossRef

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 CrossRef

20.

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

21.

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

22.

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

23.

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

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

25.

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

26.

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

27.

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

28.

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

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

30.

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

31.

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

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 CrossRef

33.

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

34.

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

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 CrossRef

Titel: Completeness for a First-Order Abstract Separation Logic
verfasst von: Zhé Hóu
Alwen Tiu
Verlag: Springer International Publishing
Buch: Programming Languages and Systems
Print ISBN: 978-3-319-47957-6

Electronic ISBN: 978-3-319-47958-3

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-47958-3_23

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner