{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T23:47:54Z","timestamp":1777765674085,"version":"3.51.4"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031974380","type":"print"},{"value":"9783031974397","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T00:00:00Z","timestamp":1756512000000},"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":[[2026]]},"DOI":"10.1007\/978-3-031-97439-7_15","type":"book-chapter","created":{"date-parts":[[2025,8,30]],"date-time":"2025-08-30T11:04:14Z","timestamp":1756551854000},"page":"301-319","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Beyond Concurrent Separation Logic: Who is Afraid of\u00a0Completeness Proofs?"],"prefix":"10.1007","author":[{"given":"Frank S.","family":"de 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,8,30]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"Amighi, A., Hurlin, C., Huisman, M., Haack, C.: Permission-based separation logic for multithreaded Java programs. Logical Methods Comput. Sci. 11 (2015)","DOI":"10.2168\/LMCS-11(1:2)2015"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/BF00289262","volume":"15","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Recursive assertions and parallel programs. Acta Informatica 15, 219\u2013232 (1981)","journal-title":"Acta Informatica"},{"key":"15_CR3","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press (2008)"},{"issue":"1\u20133","key":"15_CR4","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":"15_CR5","doi-asserted-by":"crossref","unstructured":"Brookes, S.: Syntactic control of interference and concurrent separation logic. In: Berger, U., Mislove, M.W. (eds.) Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK, 6\u20139 June 2012. Electronic Notes in Theoretical Computer Science, vol. 286, pp. 87\u2013102. Elsevier (2012)","DOI":"10.1016\/j.entcs.2012.08.007"},{"issue":"3","key":"15_CR6","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":"ACM SIGLOG News"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-71237-6_10","volume-title":"Programming Languages and Systems","author":"Q Cao","year":"2017","unstructured":"Cao, Q., Cuellar, S., Appel, A.W.: Bringing order to the separation logic jungle. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 190\u2013211. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_10"},{"key":"15_CR8","unstructured":"Cousot, P., Cousot, R.: Invariance proof methods and analysis techniques for parallel programs. In: Biermann, A.W., Guiho, G., Kodratoff, Y. (eds.) Automatic Program Construction Techniques, chapter\u00a012, pp. 243\u2013271. Macmillan, New York (1984)"},{"key":"15_CR9","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/j.tcs.2016.04.004","volume":"631","author":"M Ameen","year":"2016","unstructured":"Ameen, M., Tatsuta, M.: Completeness for recursive procedures in separation logic. Theor. Comput. Sci. 631, 73\u201396 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/3-540-08860-1_20","volume-title":"Automata, Languages and Programming","author":"D Harel","year":"1978","unstructured":"Harel, D.: Arithmetical completeness in logics of programs. In: Ausiello, G., B\u00f6hm, C. (eds.) ICALP 1978. LNCS, vol. 62, pp. 268\u2013288. Springer, Heidelberg (1978). https:\/\/doi.org\/10.1007\/3-540-08860-1_20"},{"key":"15_CR11","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"issue":"5","key":"15_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279\u2013285 (1976)","journal-title":"Commun. ACM"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bornat, R., O\u2019Hearn, P.: Modular verification of a non-blocking stack. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 297\u2013302 (2007)","DOI":"10.1145\/1190216.1190261"},{"key":"15_CR14","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), 22\u201325 July 2002, Copenhagen, Denmark, Proceedings, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1007\/978-3-319-10575-8_20","volume-title":"Handbook of Model Checking","author":"N Shankar","year":"2018","unstructured":"Shankar, N.: Combining model checking and deduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 651\u2013684. Springer, Cham (2018)"}],"container-title":["Lecture Notes in Computer Science","Principles of Formal Quantitative Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-97439-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T15:28:00Z","timestamp":1777476480000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-97439-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,30]]},"ISBN":["9783031974380","9783031974397"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-97439-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,8,30]]},"assertion":[{"value":"30 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}