{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:37:29Z","timestamp":1767926249590,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642277047","type":"print"},{"value":"9783642277054","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-27705-4_15","type":"book-chapter","created":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T12:18:06Z","timestamp":1327493886000},"page":"179-195","source":"Crossref","is-referenced-by-count":10,"title":["Formalized Verification of Snapshotable Trees: Separation and Sharing"],"prefix":"10.1007","author":[{"given":"Hannes","family":"Mehnert","sequence":"first","affiliation":[]},{"given":"Filip","family":"Sieczkowski","sequence":"additional","affiliation":[]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Sestoft","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-57155-8_236","volume-title":"Algorithms and Data Structures","author":"A. Andersson","year":"1993","unstructured":"Andersson, A.: Balanced Search Trees Made Simple. In: Dehne, F., et al. (eds.) WADS 1993. LNCS, vol.\u00a0709, pp. 60\u201371. Springer, Heidelberg (1993)"},{"key":"15_CR2","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":"15_CR3","doi-asserted-by":"crossref","unstructured":"Biering, B., Birkedal, L., Torp-Smith, N.: BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275499"},{"key":"15_CR4","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":"15_CR5","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)"},{"issue":"1","key":"15_CR6","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1016\/0022-0000(89)90034-2","volume":"38","author":"J. Driscoll","year":"1989","unstructured":"Driscoll, J., Sarnak, N., Sleator, D., Tarjan, R.: Making data structures persistent. Journal of Computer and Systems Sciences\u00a038(1), 86\u2013124 (1989)","journal-title":"Journal of Computer and Systems Sciences"},{"key":"15_CR7","first-page":"8","volume-title":"19th FCS","author":"L. Guibas","year":"1978","unstructured":"Guibas, L., Sedgewick, R.: A dichromatic framework for balanced trees. In: 19th FCS, pp. 8\u201321. Ann Arbor, Michigan (1978)"},{"key":"15_CR8","unstructured":"Kokholm, N., Sestoft, P.: The C5 Generic Collection Library for C# and CLI. Technical Report ITU-TR-2006-76, IT University of Copenhagen (January 2006)"},{"key":"15_CR9","unstructured":"Krishnaswami, N.: Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis. Carnegie Mellon University (forthcoming, 2011)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Birkedal, L., Aldrich, J.: Verifying event-driven programs using ramified frame properties. In: TLDI, pp. 63\u201376. ACM (2010)","DOI":"10.1145\/1708016.1708025"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: An Automatic Program Verifier for Functional Correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol.\u00a06355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Malecha, G., Morrisett, G.: Mechanized verification with sharing. In: 7th International Colloquium on Theoretical Aspects of Computing (September 2010)","DOI":"10.1007\/978-3-642-14808-8_17"},{"key":"15_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-642-20398-5_42","volume-title":"NASA Formal Methods","author":"H. Mehnert","year":"2011","unstructured":"Mehnert, H.: Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java Code. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 518\u2013524. Springer, Heidelberg (2011)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: dependent types for imperative programs. In: Hook, J., Thiemann, P. (eds.) Proc. of 13th ACM ICFP 2008, pp. 229\u2013240. ACM (2008)","DOI":"10.1145\/1411204.1411237"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Vafeiadis, V., Berdine, J.: Structuring the verification of heap-manipulating programs. In: Proceedings of POPL (2010)","DOI":"10.1145\/1706299.1706331"},{"key":"15_CR16","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":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78739-6_26","volume-title":"Programming Languages and Systems","author":"R.L. Petersen","year":"2008","unstructured":"Petersen, R.L., Birkedal, L., Nanevski, A., Morrisett, G.: A Realizability Model for Impredicative Hoare Type Theory. In: Gairing, M. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 337\u2013352. Springer, Heidelberg (2008)"},{"key":"15_CR18","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: IEEE Proc. of 17th Symp. on Logic in CS (November 2002)"},{"key":"15_CR19","unstructured":"Sedgewick, R.: Left-leaning red-black trees, \n                  \n                    http:\/\/www.cs.princeton.edu\/~rs\/talks\/LLRB\/LLRB.pdf"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-642-14107-2_9","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"K. Svendsen","year":"2010","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Verifying Generics and Delegates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol.\u00a06183, pp. 175\u2013199. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27705-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T12:48:39Z","timestamp":1556196519000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27705-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642277047","9783642277054"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27705-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}