{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T00:37:42Z","timestamp":1783643862181,"version":"3.55.0"},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:00:00Z","timestamp":1746230400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T00:00:00Z","timestamp":1746230400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21-CE48-0011"],"award-info":[{"award-number":["ANR-21-CE48-0011"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-21-CE48-0011"],"award-info":[{"award-number":["ANR-21-CE48-0011"]}],"id":[{"id":"10.13039\/501100001665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,6]]},"DOI":"10.1007\/s10817-025-09728-7","type":"journal-article","created":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T10:45:43Z","timestamp":1746269143000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Direct Procedure to Test Entailment in a Separation Logic of Relations"],"prefix":"10.1007","volume":"69","author":[{"given":"Mnacho","family":"Echenim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"key":"9728_CR1","doi-asserted-by":"crossref","unstructured":"Ahrens, E., Bozga, M., Iosif, R., Katoen, J.: Reasoning about distributed reconfigurable systems. In: Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, pp. 145\u2013174 (2022)","DOI":"10.1145\/3563293"},{"key":"9728_CR2","doi-asserted-by":"crossref","unstructured":"Bozga, M., Bueri, L., Iosif, R.: Decision problems in a logic for reasoning about reconfigurable distributed systems. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning\u201411th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, Volume 13385 of Lecture Notes in Computer Science, pp. 691\u2013711. Springer (2022)","DOI":"10.1007\/978-3-031-10769-6_40"},{"key":"9728_CR3","doi-asserted-by":"crossref","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Entailment checking in separation logic with inductive definitions is 2-EXPTIME hard. In: Albert, E., Kov\u00e1cs, L. (eds.) LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, Volume 73 of EPiC Series in Computing, pp. 191\u2013211. EasyChair (2020)","DOI":"10.29007\/f5wh"},{"key":"9728_CR4","doi-asserted-by":"crossref","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Decidable entailments in separation logic with inductive definitions: beyond establishment. In: CSL 2021: 29th International Conference on Computer Science Logic, EPiC Series in Computing. EasyChair (2021)","DOI":"10.1007\/978-3-030-79876-5_11"},{"key":"9728_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2021.106169","volume":"173","author":"M Echenim","year":"2022","unstructured":"Echenim, M., Iosif, R., Peltier, N.: Entailment is undecidable for symbolic heap separation logic formul\u00e6 with non-established inductive rules. Inf. Process. Lett. 173, 106169 (2022)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"9728_CR6","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/s10817-023-09680-4","volume":"67","author":"M Echenim","year":"2023","unstructured":"Echenim, M., Peltier, N.: A proof procedure for separation logic with inductive definitions and data. J. Autom. Reason. 67(3), 30 (2023)","journal-title":"J. Autom. Reason."},{"key":"9728_CR7","doi-asserted-by":"crossref","unstructured":"Iosif, R., Rogalewicz, A., Simacek, J.: The tree width of separation logic with recursive definitions. In: Proceedings of CADE-24, Volume 7898 of LNCS (2013)","DOI":"10.1007\/978-3-642-38574-2_2"},{"key":"9728_CR8","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: Bi as an assertion language for mutable data structures. In: ACM SIGPLAN Notices, vol. 36, pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"key":"9728_CR9","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Rinard, M.C.: Generalized records and spatial conjunction in role logic. In: Giacobazzi, R. (eds) Static Analysis, 11th International Symposium, SAS 2004, Verona, Italy, August 26-28, 2004, Proceedings, Volume 3148 of Lecture Notes in Computer Science, pp. 361\u2013376. Springer (2004)","DOI":"10.1007\/978-3-540-27864-1_26"},{"issue":"1","key":"9728_CR10","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/3534927","volume":"24","author":"C Matheja","year":"2023","unstructured":"Matheja, C., Pagel, J., Zuleger, F.: A decision procedure for guarded separation logic complete entailment checking for separation logic with inductive definitions. ACM Trans. Comput. Log. 24(1), 1:1-1:76 (2023)","journal-title":"ACM Trans. Comput. Log."},{"key":"9728_CR11","doi-asserted-by":"crossref","unstructured":"Pagel, J., Zuleger, F.: Beyond symbolic heaps: deciding separation logic with inductive definitions. In: LPAR-23, Volume 73 of EPiC Series in Computing, pp. 390\u2013408. EasyChair (2020)","DOI":"10.29007\/vkmj"},{"key":"9728_CR12","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS\u201902 (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09728-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09728-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09728-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T09:04:16Z","timestamp":1750669456000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09728-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,3]]},"references-count":12,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6]]}},"alternative-id":["9728"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09728-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,5,3]]},"assertion":[{"value":"14 October 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 April 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflict of interest as defined by Springer, or other interests that might be perceived to influence the results and\/or discussion reported in this paper.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"10"}}