{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:48:59Z","timestamp":1768006139020,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642148071","type":"print"},{"value":"9783642148088","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14808-8_17","type":"book-chapter","created":{"date-parts":[[2010,8,21]],"date-time":"2010-08-21T09:52:01Z","timestamp":1282384321000},"page":"245-259","source":"Crossref","is-referenced-by-count":4,"title":["Mechanized Verification with Sharing"],"prefix":"10.1007","author":[{"given":"Gregory","family":"Malecha","sequence":"first","affiliation":[]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B.E. Aydemir","year":"2005","unstructured":"Aydemir, B.E., Bohannon, A., Fairbairn, M., et al.: Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/1181195.1181212","volume-title":"SAVCBS 2006","author":"K. Bierhoff","year":"2006","unstructured":"Bierhoff, K.: Iterator specification with typestates. In: SAVCBS 2006, pp. 79\u201382. ACM, New York (2006)"},{"key":"17_CR3","unstructured":"Bornat, R., Calcagno, C., OHearn, P.: Local reasoning, separation and aliasing. In: Proceedings of SPACE, vol.\u00a04 (2004)"},{"key":"17_CR4","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1145\/1596550.1596565","volume-title":"ICFP 2009","author":"A. Chlipala","year":"2009","unstructured":"Chlipala, A., et al.: Effective interactive proofs for higher-order imperative programs. In: ICFP 2009, pp. 79\u201390. ACM, New York (2009)"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/286936.286947","volume-title":"OOPSLA 1998","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48\u201364. ACM, New York (1998)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology","author":"C. Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation Logic Contracts for a Java-Like Language with Fork\/Join. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 199\u2013215. Springer, Heidelberg (2008)"},{"issue":"10","key":"17_CR7","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Boyland, J.: Checking Interference with Fractional Permissions, vol.\u00a02694 (2003)","DOI":"10.1007\/3-540-44898-5_4"},{"key":"17_CR9","unstructured":"Jonas, B.J.: Specification and validation of data structures using separation logic. Master\u2019s thesis, Technical University of Denmark (2010)"},{"key":"17_CR10","volume-title":"SAVCBS 2009","author":"T. Kim","year":"2009","unstructured":"Kim, T., Bierhoff, K., Aldrich, J., Kang, S.: Typestate protocol specification in JML. In: SAVCBS 2009. ACM, New York (2009)"},{"key":"17_CR11","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/1181195.1181213","volume-title":"SAVCBS 2006","author":"N.R. Krishnaswami","year":"2006","unstructured":"Krishnaswami, N.R.: Reasoning about iterators with separation logic. In: SAVCBS 2006, pp. 83\u201386. ACM, New York (2006)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: POPL 2010 (January 2010)","DOI":"10.1145\/1706299.1706329"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura De","year":"2008","unstructured":"De Moura, L., Bjrner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"17_CR14","volume-title":"ICFP 2006","author":"A. Nanevski","year":"2006","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: ICFP 2006. ACM, New York (2006)"},{"issue":"1-3","key":"17_CR15","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"key":"17_CR16","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science, LICS 2002 (2002)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/j.entcs.2008.10.021","volume":"218","author":"A. Sexton","year":"2008","unstructured":"Sexton, A., Thielecke, H.: Reasoning about B+ Trees with Operational Semantics and Separation Logic. Electronic Notes in Theoretical Computer Science\u00a0218, 355\u2013369 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"issue":"8","key":"17_CR19","doi-asserted-by":"publisher","first-page":"631","DOI":"10.1109\/32.310672","volume":"20","author":"B.W. Weide","year":"1994","unstructured":"Weide, B.W., et al.: Design and Specification of Iterators Using the Swapping Paradigm. IEEE Trans. Softw. Eng.\u00a020(8), 631\u2013643 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR20","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/1181195.1181211","volume-title":"SAVCBS 2006","author":"B.W. Weide","year":"2006","unstructured":"Weide, B.W.: SAVCBS 2006 challenge: specification of iterators. In: SAVCBS 2006, pp. 75\u201377. ACM, New York (2006)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2010"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14808-8_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:20:25Z","timestamp":1558300825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14808-8_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642148071","9783642148088"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14808-8_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}