{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T16:41:15Z","timestamp":1725900075374},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642305603"},{"type":"electronic","value":"9783642305610"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30561-0_14","type":"book-chapter","created":{"date-parts":[[2012,5,25]],"date-time":"2012-05-25T18:31:43Z","timestamp":1337970703000},"page":"187-201","source":"Crossref","is-referenced-by-count":0,"title":["Verification of Snapshotable Trees Using Access Permissions and Typestate"],"prefix":"10.1007","author":[{"given":"Hannes","family":"Mehnert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1145\/199818.199860","volume":"30","author":"H.G. Baker","year":"1995","unstructured":"Baker, H.G.: \u201duse-once\u201d variables and linear objects: storage management, reflection and multi-threading. SIGPLAN Not.\u00a030, 45\u201352 (1995)","journal-title":"SIGPLAN Not."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-22655-7_2","volume-title":"ECOOP 2011 \u2013 Object-Oriented Programming","author":"N.E. Beckman","year":"2011","unstructured":"Beckman, N.E., Kim, D., Aldrich, J.: An Empirical Study of Object Protocols in the Wild. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol.\u00a06813, pp. 2\u201326. Springer, Heidelberg (2011)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Bierhoff, K.: Iterator specification with typestates. In: Proceedings of the 2006 Conference on Specification and Verification of Component-Based Systems, SAVCBS 2006, pp. 79\u201382 (2006)","DOI":"10.1145\/1181195.1181212"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Bierhoff, K.: Api protocol compliance in object-oriented software. Tech. Rep. CMU-ISR-09-108, CMU ISR SCS (2009)","DOI":"10.1145\/1449814.1449906"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Bierhoff, K.: Automated program verification made symplar. In: Proc. of Onward! 2011 (2011)","DOI":"10.1145\/2048237.2048242"},{"key":"14_CR6","unstructured":"Bierhoff, K., Aldrich, J.: Permissions to specify the composite design pattern. In: Proc. of SAVCBS 2008 (2008)"},{"key":"14_CR7","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)"},{"issue":"1","key":"14_CR8","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":"14_CR9","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":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-27705-4_15","volume-title":"Verified Software: Theories, Tools, Experiments","author":"H. Mehnert","year":"2012","unstructured":"Mehnert, H., Sieczkowski, F., Birkedal, L., Sestoft, P.: Formalized Verification of Snapshotable Trees: Separation and Sharing. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 179\u2013195. Springer, Heidelberg (2012)"},{"key":"14_CR11","unstructured":"Nistor, L., Aldrich, J.: Verifying object-oriented code using object propositions. In: Proc. of IWACO (2011)"},{"key":"14_CR12","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering (1998)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Sunshine, J., Naden, K., Stork, S., Aldrich, J., Tanter, \u00c9.: First-class state change in plaid. In: OOPSLA 2011 (2011)","DOI":"10.1145\/2048066.2048122"}],"container-title":["Lecture Notes in Computer Science","Objects, Models, Components, Patterns"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30561-0_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,22]],"date-time":"2023-06-22T19:21:18Z","timestamp":1687461678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30561-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642305603","9783642305610"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30561-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}