{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T00:10:08Z","timestamp":1750810208776,"version":"3.41.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_19","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"285-303","source":"Crossref","is-referenced-by-count":2,"title":["Proof Tactics for Assertions in Separation Logic"],"prefix":"10.1007","author":[{"given":"Zh\u00e9","family":"H\u00f3u","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"Facebook Infer. http:\/\/fbinfer.com\/"},{"key":"19_CR2","unstructured":"Isabelle\/HOL tactics for separation algebra. http:\/\/securify.scse.ntu.edu.sg\/SoftVer\/Separata"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-32347-8_21","volume-title":"Interactive Theorem Proving","author":"J Bengtson","year":"2012","unstructured":"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\u2013331. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-32347-8_21"},{"key":"19_CR4","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: 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"},{"key":"19_CR5","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). doi:10.1007\/11575467_5"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-87531-4_24","volume-title":"Computer Science Logic","author":"R Brochenin","year":"2008","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol. 5213, pp. 323\u2013338. Springer, Heidelberg (2008). doi:10.1007\/978-3-540-87531-4_24"},{"key":"19_CR7","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":"19_CR8","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, 14:1\u201314:43 (2014)","journal-title":"J. ACM"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: POPL 2014, pp. 453\u2013464 (2014)","DOI":"10.1145\/2578855.2535844"},{"issue":"6","key":"19_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 1\u201366 (2011)","journal-title":"J. ACM"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007, pp. 366\u2013378. IEEE (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-60983-0_5","volume-title":"Extensions of Logic Programming","author":"I Cervesato","year":"1996","unstructured":"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\u201381. Springer, Heidelberg (1996). doi:10.1007\/3-540-60983-0_5"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11538363_15","volume-title":"Computer Science Logic","author":"K Chaudhuri","year":"2005","unstructured":"Chaudhuri, K., Pfenning, F.: Focusing the inverse method for linear logic. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 200\u2013215. Springer, Heidelberg (2005). doi:10.1007\/11538363_15"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI 2011, pp. 234\u2013245 (2011)","DOI":"10.1145\/1993316.1993526"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Chlipala, A., Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Effective interactive proofs for higher-order imperative programs. In: ICFP 2009 (2009)","DOI":"10.1145\/1596550.1596565"},{"key":"19_CR16","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"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Feng, X.: Local rely-guarantee reasoning. In POPL 2009, pp. 315\u2013327. ACM (2009)","DOI":"10.1145\/1594834.1480922"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/11944836_33","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"D Galmiche","year":"2006","unstructured":"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\u2013368. Springer, Heidelberg (2006). doi:10.1007\/11944836_33"},{"key":"19_CR19","unstructured":"Ronghui, G., Shao, Z., Chen, H., Xiongnan, W., Kim, J., Sj\u00f6berg, V., Costanzo, D.: Certikos: an extensible architecture for building certified concurrent OS kernels. In OSDI 2016, pp. 653\u2013669 (2016)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-45793-3_12","volume-title":"Computer Science Logic","author":"JS Hodas","year":"2002","unstructured":"Hodas, J.S., L\u00f3pez, 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\u2013182. Springer, Heidelberg (2002). doi:10.1007\/3-540-45793-3_12"},{"key":"19_CR21","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 (2014)","DOI":"10.1145\/2535838.2535864"},{"key":"19_CR22","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, Cham (2015). doi:10.1007\/978-3-319-21401-6_34"},{"key":"19_CR23","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). doi:10.1007\/978-3-642-40537-2_16"},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/978-3-319-47958-3_23","volume-title":"Programming Languages and Systems","author":"Z H\u00f3u","year":"2016","unstructured":"H\u00f3u, Z., Tiu, A.: Completeness for a first-order abstract separation logic. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 444\u2013463. Springer, Cham (2016). doi:10.1007\/978-3-319-47958-3_23"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-32347-8_22","volume-title":"Interactive Theorem Proving","author":"G Klein","year":"2012","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 332\u2013337. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-32347-8_22"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-662-54434-1_26","volume-title":"Programming Languages and Systems","author":"R Krebbers","year":"2017","unstructured":"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\u2013723. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54434-1_26"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: POPL 2017, pp. 205\u2013217 (2017)","DOI":"10.1145\/3093333.3009855"},{"key":"19_CR28","unstructured":"Lammich, P., Meis, R.: A separation logic framework for imperative HOL. In: AFP 2012 (2012)"},{"issue":"1","key":"19_CR29","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2422085.2422091","volume":"14","author":"D Larchey-Wendling","year":"2013","unstructured":"Larchey-Wendling, D., Galmiche, D.: Non-deterministic phase semantics and the undecidability of Boolean BI. ACM TOCL 14(1), 6:1\u20136:41 (2013)","journal-title":"ACM TOCL"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"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\u2013429, May 2013","DOI":"10.1109\/SP.2013.35"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-14052-5_34","volume-title":"Interactive Theorem Proving","author":"MO Myreen","year":"2010","unstructured":"Myreen, M.O.: Separation logic adapted for proofs by rewriting. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 485\u2013489. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14052-5_34"},{"key":"19_CR32","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, 215\u2013244 (1999)","journal-title":"BSL"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Park, J., Seo, J., Park, S.: A theorem prover for Boolean BI. In: POPL 2013, pp. 219\u2013232 (2013)","DOI":"10.1145\/2480359.2429095"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In LICS 2002, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"19_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-662-54577-5_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D San\u00e1n","year":"2017","unstructured":"San\u00e1n, 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\u2013498. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54577-5_28"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In PLDI 2015, pp. 77\u201387 (2015)","DOI":"10.1145\/2813885.2737964"},{"key":"19_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-03359-9_32","volume-title":"Theorem Proving in Higher Order Logics","author":"T Tuerk","year":"2009","unstructured":"Tuerk, T.: A formalisation of smallfoot in HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 469\u2013484. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-03359-9_32"},{"key":"19_CR38","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Cambridge Technical report, vol. 687 (2007)"},{"key":"19_CR39","first-page":"371","volume":"218","author":"C Varming","year":"2008","unstructured":"Varming, C., Birkedal, L.: Higher-order separation logic in Isabelle\/HOLCF. ENTCS 218, 371\u2013389 (2008)","journal-title":"ENTCS"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:39:01Z","timestamp":1750808341000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}