{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:54:25Z","timestamp":1766134465093,"version":"3.48.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T00:00:00Z","timestamp":1759104000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T00:00:00Z","timestamp":1759104000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The basic set-theoretic interpretation of the separating connectives of first-order separation logic allows for an effective, sound and complete axiomatization in a hybrid extension.<\/jats:p>","DOI":"10.1007\/s10817-025-09739-4","type":"journal-article","created":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T14:46:15Z","timestamp":1759157175000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["First-order\u00a0Hybrid\u00a0Separation\u00a0Logic"],"prefix":"10.1007","volume":"69","author":[{"given":"Frank S. de","family":"Boer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hans-Dieter A.","family":"Hiep","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,29]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In Computer Aided Verification: 23rd International Conference, CAV 2011, volume 6806 of LNCS, pages 178\u2013183. Springer, (2011)","key":"9739_CR1","DOI":"10.1007\/978-3-642-22110-1_15"},{"issue":"1","key":"9739_CR2","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1145\/1047659.1040327","volume":"40","author":"R Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. SIGPLAN Notices 40(1), 259\u2013270 (2005)","journal-title":"SIGPLAN Notices"},{"key":"9739_CR3","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. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"issue":"3","key":"9739_CR4","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/2984450.2984457","volume":"3","author":"S Brookes","year":"2016","unstructured":"Brookes, S., O\u2019Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47\u201365 (2016)","journal-title":"Concurrent separation logic. ACM SIGLOG News"},{"doi-asserted-by":"crossref","unstructured":"Brotherston, J., Villard, J: Parametric completeness for separation theories. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, San Diego, CA, USA, January 20-21, 2014, pages 453\u2013464. ACM, (2014)","key":"9739_CR5","DOI":"10.1145\/2535838.2535844"},{"doi-asserted-by":"crossref","unstructured":"de\u00a0Boer, F.\u00a0S., Hiep, H.-D.\u00a0A., de\u00a0Gouw, S.: The logic of separation logic: Models and proofs. In Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference TABLEAUX, volume 14278 of LNCS, pages 407\u2013426. Springer, (2023)","key":"9739_CR6","DOI":"10.1007\/978-3-031-43513-3_22"},{"doi-asserted-by":"crossref","unstructured":"Demri, S., Lozes, \u00c9., Mansutti, A.: A complete axiomatisation for quantifier-free separation logic. Logical Methods in Computer Science, 17(3), (2021)","key":"9739_CR7","DOI":"10.46298\/lmcs-17(3:17)2021"},{"issue":"1","key":"9739_CR8","doi-asserted-by":"publisher","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. Log. Comput. 20(1), 189\u2013231 (2010)","journal-title":"J. Log. Comput."},{"issue":"2","key":"9739_CR9","first-page":"134","volume":"1","author":"AS George","year":"2024","unstructured":"George, A.S.: When trust fails: Examining systemic risk in the digital economy from the 2024 CrowdStrike outage. Partners Universal Multidisciplinary Research Journal 1(2), 134\u2013152 (2024)","journal-title":"Partners Universal Multidisciplinary Research Journal"},{"doi-asserted-by":"crossref","unstructured":"Gries, D., Schneider, F.B.: Avoiding the undefined by underspecification. In Computer Science Today: Recent Trends and Developments, volume 1000 of LNCS, pages 366\u2013373. Springer, (1995)","key":"9739_CR10","DOI":"10.1007\/BFb0015254"},{"doi-asserted-by":"crossref","unstructured":"Hance, T., Howell, J., Padon, O., Parno, B.: Leaf: Modularity for temporary sharing in separation logic. Proceedings of the ACM on Programming Languages, 7(OOPSLA2), (2023)","key":"9739_CR11","DOI":"10.1145\/3622798"},{"doi-asserted-by":"crossref","unstructured":"Henkin, L: Completeness in the theory of types. The Journal of Symbolic Logic, 15(2), (1950)","key":"9739_CR12","DOI":"10.2307\/2266967"},{"issue":"3","key":"9739_CR13","doi-asserted-by":"publisher","first-page":"159","DOI":"10.2307\/2267044","volume":"14","author":"L Henkin","year":"1949","unstructured":"Henkin, L.: The completeness of the first-order functional calculus. J. Symb. Log. 14(3), 159\u2013166 (1949)","journal-title":"J. Symb. Log."},{"key":"9739_CR14","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.14635180","author":"H-DA Hiep","year":"2025","unstructured":"Hiep, H.-D.A.: The logic of separation logic: First-order hybrid separation logic (Coq artifact) (2025). https:\/\/doi.org\/10.5281\/zenodo.14635180","journal-title":"The logic of separation logic: First-order hybrid separation logic (Coq artifact)"},{"doi-asserted-by":"crossref","unstructured":"Hou, Z., Tiu, A.: Completeness for a first-order abstract separation logic. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, volume 10017 of LNCS, pages 444\u2013463, (2016)","key":"9739_CR15","DOI":"10.1007\/978-3-319-47958-3_23"},{"doi-asserted-by":"crossref","unstructured":"Huet, G.\u00a0P., Herbelin, H.: 30 years of research and development around Coq. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 249\u2013250. ACM, (2014)","key":"9739_CR16","DOI":"10.1145\/2535838.2537848"},{"doi-asserted-by":"crossref","unstructured":"Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28, (2018)","key":"9739_CR17","DOI":"10.1017\/S0956796818000151"},{"unstructured":"Krishnaswami, N.\u00a0R.: A modal sequent calculus for propositional separation logic, (2008). (Draft)","key":"9739_CR18"},{"issue":"119","key":"9739_CR19","first-page":"2016","volume":"1","author":"Luca Aceto. Interview with Stephen Brookes and Peter W. O\u2019Hearn, recipients of the","year":"2016","unstructured":"Luca Aceto. Interview with Stephen Brookes and Peter W. O\u2019Hearn, recipients of the: G\u00f6del prize. Bulletin of EATCS 1(119), 2016 (2016)","journal-title":"Bulletin of EATCS"},{"unstructured":"Mansutti, A.: Reasoning with Separation Logics. PhD thesis, \u00c9cole Normale Sup\u00e9rieure, France, (2020)","key":"9739_CR20"},{"doi-asserted-by":"crossref","unstructured":"Mugu, S\u00a0R., Zhang, B., Kolla, H., Balaji, S.R.A., Ranganathan, P.: Lessons from the CrowdStrike incident: Assessing endpoint security vulnerabilities and implications. In 2024 Cyber Awareness and Research Symposium (CARS), 1\u201310, (2024)","key":"9739_CR21","DOI":"10.1109\/CARS61786.2024.10778784"},{"issue":"2","key":"9739_CR22","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3211968","volume":"62","author":"P O\u2019Hearn","year":"2019","unstructured":"O\u2019Hearn, P.: Separation logic. Communications of the ACM 62(2), 86\u201395 (2019)","journal-title":"Communications of the ACM"},{"doi-asserted-by":"crossref","unstructured":"Pym, D.J.: The semantics and proof theory of the logic of bunched implications, volume\u00a026 of Applied Logic Series. Springer, (2002)","key":"9739_CR23","DOI":"10.1007\/978-94-017-0091-7"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., Serban, C., King,T.: A decision procedure for separation logic in SMT. In International Symposium on Automated Technology for Verification and Analysis, volume 9938 of LNCS, pages 244\u2013261. Springer, (2016)","key":"9739_CR24","DOI":"10.1007\/978-3-319-46520-3_16"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: An overview of separation logic. In Verified Software: Theories, Tools, Experiments, First IFIP TC 2\/WG 2.3 Conference, VSTTE 2005, volume 4171 of LNCS, pages 460\u2013469. Springer, (2005)","key":"9739_CR25","DOI":"10.1007\/978-3-540-69149-5_49"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pages 55\u201374. IEEE Computer Society, (2002)","key":"9739_CR26","DOI":"10.1109\/LICS.2002.1029817"},{"unstructured":"Torben Bra\u00fcner. Hybrid Logic. In Edward\u00a0N. Zalta and Uri Nodelman, editors, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Summer 2024 edition, 2024","key":"9739_CR27"},{"unstructured":"van Starkenburg, B., Basold, H., Ford, C.: Separation logic of generic resources via sheafeology. arXiv preprint arXiv:2508.01866, (2025)","key":"9739_CR28"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09739-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09739-4","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09739-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:50:31Z","timestamp":1766134231000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09739-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,29]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9739"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09739-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,9,29]]},"assertion":[{"value":"24 April 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 September 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 September 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Statements and Declarations"}},{"value":"The authors declare to have no competing interests as defined by Springer, or other interests that might be perceived to influence the results and\/or discussion reported in this paper. The results\/data\/figures in this manuscript have not been published elsewhere, nor are they under consideration by another publisher. The manuscript does not contain any material from third parties. This manuscript does not report data generation or analysis. The authors Frank\u00a0S.\u00a0de\u00a0Boer and Hans-Dieter\u00a0A.\u00a0Hiep contributed equally to this work. There is no funding to declare.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"26"}}