{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:28:41Z","timestamp":1770290921577,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_19","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"377-396","source":"Crossref","is-referenced-by-count":44,"title":["Fictional Separation Logic"],"prefix":"10.1007","author":[{"given":"Jonas Braband","family":"Jensen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-22863-6_5","volume-title":"Interactive Theorem Proving","author":"J. Bengtson","year":"2011","unstructured":"Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 22\u201338. Springer, Heidelberg (2011)"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Transactions on Programming Languages and Systems\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for algol-like languages. Logical Methods in Computer Science 2(5:1) (August 2006)","DOI":"10.2168\/LMCS-2(5:1)2006"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: Proceedings of POPL, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking Interference with Fractional Permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proceedings of LICS (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent Abstract Predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 504\u2013528. Springer, Heidelberg (2010)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-15057-9_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Gardner, P., Wheelhouse, M.: Abstraction and Refinement for Local Reasoning. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 199\u2013215. Springer, Heidelberg (2010)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Dinsdale-Young, T., Gardner, P., Wheelhouse, M.: Abstraction and refinement for local reasoning (February 2011); journal submission","DOI":"10.1007\/978-3-642-15057-9_14"},{"key":"19_CR10","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.\u00a05904, pp. 161\u2013177. Springer, Heidelberg (2009)"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: Proceedings of POPL (2011)","DOI":"10.1145\/1926385.1926416"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B.: Precision and the conjunction rule in concurrent separation logic. In: Proceedings of MFPS (2011)","DOI":"10.1016\/j.entcs.2011.09.021"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Haack, C., Hurlin, C.: Resource usage protocols for iterators. In: Proceedings of IWACO (2008)","DOI":"10.5381\/jot.2009.8.4.a3"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Jensen, J.B., Birkedal, L.: Fictional separation logic: Appendix (2011), http:\/\/itu.dk\/~jobr\/research\/fsl-appendix.pdf","DOI":"10.1007\/978-3-642-28869-2_19"},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.5381\/jot.2011.10.1.a2","volume":"10","author":"J.B. Jensen","year":"2011","unstructured":"Jensen, J.B., Birkedal, L., Sestoft, P.: Modular verification of linked lists with views via separation logic. Journal of Object Technology\u00a010, 2:1\u20132:20 (2011)","journal-title":"Journal of Object Technology"},{"key":"19_CR16","unstructured":"Krishnaswami, N.R.: Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. Ph.D. thesis, Carnegie Mellon University (2011)"},{"key":"19_CR17","unstructured":"Meyers, S.: More Effective C++: 35 New Ways to Improve Your Programs and Designs, 1st edn. Addison-Wesley Professional (1996)"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Proceedings of POPL, pp. 247\u2013258 (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: Proceedings of TLDI (2011)","DOI":"10.1145\/1929553.1929565"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-04027-6_32","volume-title":"Computer Science Logic","author":"J. Schwinghammer","year":"2009","unstructured":"Schwinghammer, J., Birkedal, L., Reus, B., Yang, H.: Nested Hoare Triples and Frame Rules for Higher-Order Store. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 440\u2013454. Springer, Heidelberg (2009)"}],"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-642-28869-2_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,23]],"date-time":"2025-03-23T18:48:42Z","timestamp":1742755722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}