{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:35:51Z","timestamp":1777890951798,"version":"3.51.4"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_34","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"501-516","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Automated Theorem Proving for Assertions in Separation Logic with All Connectives"],"prefix":"10.1007","author":[{"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rajeev","family":"Gor\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J Berdine","year":"2005","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)"},{"key":"34_CR3","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1016\/j.entcs.2006.04.006","volume":"158","author":"J Berdine","year":"2006","unstructured":"Berdine, J., O\u2019Hearn, P.W.: Strong update, disposal, and encapsulation in bunched typing. Electron. Notes Theor. Comput. Sci. 158, 81\u201398 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., Yang, H.: Variables as resource in separation logic. In: MFPS, vol. 155 of ENTCS, pp. 247\u2013276 (2006)","DOI":"10.1016\/j.entcs.2005.11.059"},{"key":"34_CR5","doi-asserted-by":"publisher","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. Inform. Comput. 211, 106\u2013137 (2012)","journal-title":"Inform. Comput."},{"issue":"1\u20133","key":"34_CR6","doi-asserted-by":"publisher","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":"34_CR7","series-title":"Lecture Notes in Computer Science","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, vol. 6803, pp. 131\u2013146. Springer, Heidelberg (2011)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-642-35182-2_25","volume-title":"Programming Languages and Systems","author":"J Brotherston","year":"2012","unstructured":"Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 350\u2013367. Springer, Heidelberg (2012)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-74061-2_15","volume-title":"Static Analysis","author":"C Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233\u2013248. Springer, Heidelberg (2007)"},{"key":"34_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-45294-X_10","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"C Calcagno","year":"2001","unstructured":"Calcagno, C., Yang, H., O\u2019Hearn, P.W.: Computability and complexity results for a spatial assertion language for data structures. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Demri, S., Deters, M.: Expressive completeness of separation logic with two variables and no separating conjunction. In: CSL\/LICS, Vienna (2014)","DOI":"10.1145\/2603088.2603142"},{"key":"34_CR13","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1449955.1449782","volume":"43","author":"D Distefano","year":"2008","unstructured":"Distefano, D., Matthew, P.: jStar: towards practical verification for java. ACM Sigplan Not. 43, 213\u2013226 (2008)","journal-title":"ACM Sigplan Not."},{"key":"34_CR14","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)"},{"issue":"1","key":"34_CR15","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1093\/logcom\/exn066","volume":"20","author":"D Galmiche","year":"2007","unstructured":"Galmiche, D., M\u00e9ry, D.: Tableaux and resource graphs for separation logic. J. Logic Comput. 20(1), 189\u2013231 (2007)","journal-title":"J. Logic Comput."},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"Hobor, A., Villard, J.: The ramifications of sharing in data structures. In: POPL 2013, pp. 523\u2013536. ACM, New York, NY, USA (2013)","DOI":"10.1145\/2480359.2429131"},{"key":"34_CR17","unstructured":"H\u00f3u, Z.: Separata+. http:\/\/users.cecs.anu.edu.au\/zhehou\/"},{"key":"34_CR18","unstructured":"H\u00f3u, Z.: Labelled Sequent Calculi and Automated Reasoning for Assertions in Separation Logic. Ph.D. thesis, The Australian National University (2015). Submitted"},{"key":"34_CR19","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, pp. 465\u2013476. ACM (2014)","DOI":"10.1145\/2578855.2535864"},{"key":"34_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-40537-2_16","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"Z H\u00f3u","year":"2013","unstructured":"H\u00f3u, Z., Tiu, A., Gor\u00e9, 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\u2013187. Springer, Heidelberg (2013)"},{"key":"34_CR21","unstructured":"Jensen, J.: Techniques for model construction in separation logic. Report (2013)"},{"key":"34_CR22","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.) Programming Languages and Systems. LNCS, vol. 7211, pp. 377\u2013396. Springer, Heidelberg (2012)"},{"key":"34_CR23","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"},{"key":"34_CR24","doi-asserted-by":"crossref","unstructured":"Lee, W., Park, S.: A proof system for separation logic with magic wand. In: POPL 2014, pp. 477\u2013490. ACM, New York, NY, USA (2014)","DOI":"10.1145\/2578855.2535871"},{"key":"34_CR25","doi-asserted-by":"crossref","unstructured":"Maclean, E., Ireland, A., Grov, G.: Proof automation for functional correctness in separation log. J. Logic Comput. (2014)","DOI":"10.1093\/logcom\/exu032"},{"key":"34_CR26","doi-asserted-by":"crossref","unstructured":"Maeda, T., Sato, H., Yonezawa, A.: Extended alias type system using separating implication. In: TLDI 2011, pp. 29\u201342. ACM, New York, NY, USA (2011)","DOI":"10.1145\/1929553.1929559"},{"key":"34_CR27","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: PLDI 2011, pp. 556\u2013566. ACM, USA (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"34_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-319-03542-0_7","volume-title":"Programming Languages and Systems","author":"JA Navarro P\u00e9rez","year":"2013","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 90\u2013106. Springer, Heidelberg (2013)"},{"issue":"2","key":"34_CR29","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"PW O\u2019Hearn","year":"1999","unstructured":"O\u2019Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symbolic Logic 5(2), 215\u2013244 (1999)","journal-title":"Bull. Symbolic Logic"},{"key":"34_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"PW O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"34_CR31","unstructured":"Parkinson, M., Bornat, R., Calcagno, C.: Variables as resource in hoare logics. In: 21st LICS (2006)"},{"key":"34_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/11874683_38","volume-title":"Computer Science Logic","author":"B Reus","year":"2006","unstructured":"Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 575\u2013590. Springer, Heidelberg (2006)"},{"key":"34_CR33","unstructured":"Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millennial Perspectives in Computer Science, pp. 303\u2013321. Palgrave (2000)"},{"key":"34_CR34","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":"34_CR35","doi-asserted-by":"crossref","unstructured":"Stewart, G., Beringer, L., Appel, A.W.: Verified heap theorem prover by paramodulation. In: ICFP, pp. 3\u201314. ACM (2012)","DOI":"10.1145\/2398856.2364531"},{"key":"34_CR36","doi-asserted-by":"crossref","unstructured":"Thakur, A., Breck, J., Reps, T.: Satisfiability modulo abstraction for separation logic with linked lists. Technical report. University of Wisconsin (2014)","DOI":"10.1145\/2632362.2632376"},{"key":"34_CR37","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)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T17:11:36Z","timestamp":1748538696000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}