{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:32:43Z","timestamp":1766136763708},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319479576"},{"type":"electronic","value":"9783319479583"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47958-3_23","type":"book-chapter","created":{"date-parts":[[2016,10,8]],"date-time":"2016-10-08T09:40:52Z","timestamp":1475919652000},"page":"444-463","source":"Crossref","is-referenced-by-count":4,"title":["Completeness for a First-Order Abstract Separation Logic"],"prefix":"10.1007","author":[{"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,9]]},"reference":[{"key":"23_CR1","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, 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\u2013137. Springer, Heidelberg (2006). doi: 10.1007\/11804192_6","DOI":"10.1007\/11804192_6"},{"key":"23_CR2","doi-asserted-by":"publisher","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52\u201368. Springer, Heidelberg (2005). doi: 10.1007\/11575467_5","DOI":"10.1007\/11575467_5"},{"key":"23_CR3","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1016\/j.ic.2011.12.003","volume":"211","author":"R Brochenin","year":"2012","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"issue":"1\u20133","key":"23_CR4","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR5","first-page":"197","volume":"265","author":"J Brotherston","year":"2010","unstructured":"Brotherston, J.: A unified display proof theory for bunched logic. ENTCS 265, 197\u2013211 (2010)","journal-title":"ENTCS"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-22438-6_12","volume-title":"Automated Deduction \u2013 CADE-23","author":"J Brotherston","year":"2011","unstructured":"Brotherston, J., Distefano, D., Petersen, R.L.: Automated cyclic entailment proofs in separation logic. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 131\u2013146. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_12"},{"issue":"2","key":"23_CR7","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2542667","volume":"61","author":"J Brotherston","year":"2014","unstructured":"Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. J. ACM 61(2), 14:1\u201314:43 (2014). doi: 10.1145\/2542667","journal-title":"J. ACM"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: POPL, pp. 453\u2013464. ACM (2014)","DOI":"10.1145\/2535838.2535844"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS, pp. 366\u2013378. IEEE (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"23_CR10","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, 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\u2013119. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45294-X_10","DOI":"10.1007\/3-540-45294-X_10"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Demri, S., Deters, M.: Expressive completeness of separation logic with two variables and no separating conjunction. In: CSL\/LICS (2014)","DOI":"10.1145\/2603088.2603142"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-06686-8_10","volume-title":"Computer Science - Theory and Applications","author":"S Demri","year":"2014","unstructured":"Demri, S., Galmiche, D., Larchey-Wendling, D., M\u00e9ry, D.: Separation logic with one quantified variable. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.\u00c9., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 125\u2013138. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-06686-8_10"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","volume-title":"Programming Languages and Systems","author":"R Dockins","year":"2009","unstructured":"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\u2013177. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-10672-9_13"},{"issue":"6","key":"23_CR14","first-page":"1033","volume":"15","author":"D Galmiche","year":"2005","unstructured":"Galmiche, D., M\u00e9ry, D., Pym, D.: The semantics of BI and resource tableaux. MSCS 15(6), 1033\u20131088 (2005)","journal-title":"MSCS"},{"issue":"1","key":"23_CR15","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1093\/logcom\/exn066","volume":"20","author":"D Galmiche","year":"2010","unstructured":"Galmiche, D., M\u00e9ry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189\u2013231 (2010)","journal-title":"J. Logic Comput."},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"H\u00f3u, Z., Clouston, R., Gor\u00e9, R., Tiu, A.: Proof search for propositional abstract separation logics via labelled sequents. In: POPL (2014)","DOI":"10.1145\/2535838.2535864"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-319-21401-6_34","volume-title":"Automated Deduction \u2013 CADE-25","author":"Z H\u00f3u","year":"2015","unstructured":"H\u00f3u, Z., Gor\u00e9, 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\u2013516. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-21401-6_34"},{"key":"23_CR18","unstructured":"H\u00f3u, Z., Tiu, A.: Completeness for a first-order abstract separation logic [cs.LO] (2016). arXiv: 1608.06729"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-642-28869-2_19","volume-title":"Programming Languages and Systems","author":"JB Jensen","year":"2012","unstructured":"Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 377\u2013396. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28869-2_19"},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R.: Reasoning about iterators with separation logic. In: SAVCBS, pp. 83\u201386. ACM (2006)","DOI":"10.1145\/1181195.1181213"},{"issue":"2","key":"23_CR21","first-page":"605","volume":"26","author":"D Larchey-Wendling","year":"2014","unstructured":"Larchey-Wendling, D.: The formal strong completeness of partial monoidal Boolean BI. JLC 26(2), 605\u2013640 (2014)","journal-title":"JLC"},{"issue":"3","key":"23_CR22","first-page":"435","volume":"19","author":"D Larchey-Wendling","year":"2009","unstructured":"Larchey-Wendling, D., Galmiche, D.: Exploring the relation between intuitionistic BI and Boolean BI: an unexpected embedding. MSCS 19(3), 435\u2013500 (2009)","journal-title":"MSCS"},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"Larchey-Wendling, D., Galmiche, D.: The undecidability of Boolean BI through phase semantics. In: LICS, pp. 140\u2013149 (2010)","DOI":"10.1109\/LICS.2010.18"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-662-44602-7_25","volume-title":"Theoretical Computer Science","author":"D Larchey-Wendling","year":"2014","unstructured":"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\u2013340. Springer, Heidelberg (2014). doi: 10.1007\/978-3-662-44602-7_25"},{"key":"23_CR25","doi-asserted-by":"crossref","unstructured":"Lee, W., Park, S.: A proof system for separation logic with magic wand. In: POPL, pp. 477\u2013490. ACM (2014)","DOI":"10.1145\/2535838.2535871"},{"key":"23_CR26","doi-asserted-by":"crossref","unstructured":"Maeda, T., Sato, H., Yonezawa, A.: Extended alias type system using separating implication. In: TLDI, pp. 29\u201342. ACM (2011)","DOI":"10.1145\/1929553.1929559"},{"key":"23_CR27","unstructured":"P\u00e9rez, J.A.N., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI. ACM (2011)"},{"issue":"2","key":"23_CR28","first-page":"215","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. BSL 5(2), 215\u2013244 (1999)","journal-title":"BSL"},{"key":"23_CR29","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). doi: 10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"23_CR30","doi-asserted-by":"crossref","unstructured":"Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL 2013, New York, NY, USA, pp. 219\u2013232 (2013)","DOI":"10.1145\/2429069.2429095"},{"key":"23_CR31","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-58025-5_65","volume-title":"Extensions of Logic Programming","author":"Peter Schroeder-Heister","year":"1994","unstructured":"Schroeder-Heister, Peter: Definitional reflection and the completion. In: Dyckhoff, Roy (ed.) ELP 1993. LNCS, vol. 798, pp. 333\u2013347. Springer, Heidelberg (1994). doi: 10.1007\/3-540-58025-5_65"},{"key":"23_CR33","doi-asserted-by":"crossref","unstructured":"Thakur, A., Breck, J., Reps, T.: Satisfiability modulo abstraction for separation logic with linked lists. In: SPIN 2014, pp. 58\u201367 (2014)","DOI":"10.1145\/2632362.2632376"},{"key":"23_CR34","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, New York (1996)"},{"key":"23_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V Vafeiadis","year":"2007","unstructured":"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\u2013271. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74407-8_18"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47958-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:40:33Z","timestamp":1498336833000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47958-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319479576","9783319479583"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47958-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}