{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:29:56Z","timestamp":1784845796192,"version":"3.55.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319127354","type":"print"},{"value":"9783319127361","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_17","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T14:53:24Z","timestamp":1413212004000},"page":"314-333","source":"Crossref","is-referenced-by-count":23,"title":["Compositional Entailment Checking for a Fragment of Separation Logic"],"prefix":"10.1007","author":[{"given":"Constantin","family":"Enea","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ond\u0159ej","family":"Leng\u00e1l","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/978-3-540-30538-5_9","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Berdine","year":"2004","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: A decidable fragment of separation logic. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 97\u2013109. Springer, Heidelberg (2004)"},{"key":"17_CR2","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.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"17_CR3","unstructured":"Brotherston, J., Fuhs, C., Gorogiannis, N., P\u00e9rez, J.N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: Proceedings of CSL-LICS. ACM (to appear, 2014)"},{"key":"17_CR4","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.\u00a07705, pp. 350\u2013367. Springer, Heidelberg (2012)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a02245, pp. 108\u2013119. Springer, Heidelberg (2001)"},{"issue":"9","key":"17_CR6","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W.-N. Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program.\u00a077(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Program."},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-642-23217-6_16","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"B. Cook","year":"2011","unstructured":"Cook, B., Haase, C., Ouaknine, J., Parkinson, M., Worrell, J.: Tractable reasoning in a fragment of separation logic. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 235\u2013249. Springer, Heidelberg (2011)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Enea, C., Leng\u00e1l, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. Technical Report FIT-TR-2014-01, FIT BUT (2014), http:\/\/www.fit.vutbr.cz\/~ilengal\/pub\/FIT-TR-2014-01.pdf","DOI":"10.1007\/978-3-319-12736-1_17"},{"key":"17_CR9","unstructured":"Enea, C., Leng\u00e1l, O., Sighireanu, M., Vojnar, T.: Spen (2014), http:\/\/www.liafa.univ-paris-diderot.fr\/spen"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Enea, C., Saveluc, V., Sighireanu, M.: Compositional invariant checking for overlaid and nested linked lists. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol.\u00a07792, pp. 129\u2013148. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-37036-6_9"},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/j.entcs.2011.09.021","volume":"276","author":"A. Gotsman","year":"2011","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Precision and the conjunction rule in concurrent separation logic. Electronic Notes in Theoretical Computer Science\u00a0276, 171\u2013190 (2011)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-319-11936-6_15","volume-title":"Proc. of ATVA 2014","author":"R. Iosif","year":"2014","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol.\u00a08837, pp. 201\u2013218. Springer, Heidelberg (2014)"},{"key":"17_CR13","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-38574-2_2","volume-title":"Automated Deduction \u2013 CADE-24","author":"R. Iosif","year":"2013","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol.\u00a07898, pp. 21\u201338. Springer, Heidelberg (2013)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14\u201326. ACM (2001)","DOI":"10.1145\/373243.375719"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-28756-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O. Leng\u00e1l","year":"2012","unstructured":"Leng\u00e1l, O., \u0160im\u00e1\u010dek, J., Vojnar, T.: VATA: A library for efficient manipulation of non-deterministic tree automata. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 79\u201394. Springer, Heidelberg (2012)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic + superposition calculus = heap theorem prover. In: Proc. of PLDI 2011, pp. 556\u2013566. ACM (2011)","DOI":"10.1145\/1993316.1993563"},{"key":"17_CR17","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":"J.A. Navarro P\u00e9rez","year":"2013","unstructured":"Navarro P\u00e9rez, J.A., Rybalchenko, A.: Separation logic modulo theories. In: Shan, C.-C. (ed.) APLAS 2013. LNCS, vol.\u00a08301, pp. 90\u2013106. Springer, Heidelberg (2013)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"773","DOI":"10.1007\/978-3-642-39799-8_54","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2013","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic using SMT. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 773\u2013789. Springer, Heidelberg (2013)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1007\/978-3-319-08867-9_47","volume-title":"Computer Aided Verification","author":"R. Piskac","year":"2014","unstructured":"Piskac, R., Wies, T., Zufferey, D.: Automating separation logic with trees and data. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 711\u2013728. Springer, Heidelberg (2014)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Qiu, X., Garg, P., Stefanescu, A., Madhusudan, P.: Natural proofs for structure, data, and separation. In: PLDI, pp. 231\u2013242. ACM (2013)","DOI":"10.1145\/2499370.2462169"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. of LICS 2002, pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"}],"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-12736-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T03:47:35Z","timestamp":1746416855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}