{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:55:28Z","timestamp":1725562528285},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_13","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"183-198","source":"Crossref","is-referenced-by-count":4,"title":["Local Reasoning and Dynamic Framing for the Composite Pattern and Its Clients"],"prefix":"10.1007","author":[{"given":"Stan","family":"Rosenberg","sequence":"first","affiliation":[]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[]},{"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 387\u2013411. Springer, Heidelberg (2008)"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","first-page":"177","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Barnett","year":"2008","unstructured":"Barnett, M., Banerjee, A., Naumann, D.A.: Boogie meets regions: a verification experience report. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 177\u2013191. Springer, Heidelberg (2008)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-540-69149-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"M. Barnett","year":"2008","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# programming system: Challenges and directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 144\u2013152. Springer, Heidelberg (2008)"},{"key":"13_CR4","unstructured":"Bierhoff, K., Aldrich, J.: Permissions to specify the composite design pattern. In: [18]"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Bierman, G., Parkinson, M.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"13_CR6","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.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, 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":"13_CR7","volume-title":"Design Patterns: Elements of Reusable Object-Oriented Software","author":"E. Gamma","year":"1995","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)"},{"key":"13_CR8","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proofs of correctness of data representations. Acta Inf.\u00a01, 271\u2013281 (1972)","journal-title":"Acta Inf."},{"key":"13_CR9","unstructured":"Jacobs, B., Smans, J., Piessens, F.: Verifying the composite pattern using separation logic. In: [18]"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"I.T. Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic framing: Support for framing, dependencies and sharing without restriction. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"issue":"2","key":"13_CR11","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing\u00a019(2), 159\u2013189 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., M\u00fcller, P.: Information hiding and visibility in interface specifications. In: ICSE (2007)","DOI":"10.1109\/ICSE.2007.44"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: LPAR (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"13_CR14","unstructured":"Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (2010)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: SAC (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013515. Springer, Heidelberg (2004)"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"13_CR18","unstructured":"Robby et al: Proc.\u00a0Seventh SAVCBS Workshop. Technical Report CS-TR-08-07, School of Electrical Engineering and Computer Science, University of Central Florida (2008)"},{"issue":"3","key":"13_CR19","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P. M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Programming\u00a062(3), 253\u2013286 (2006)","journal-title":"Sci. Comput. Programming"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-11957-6_2","volume-title":"Programming Languages and Systems","author":"D.A. Naumann","year":"2010","unstructured":"Naumann, D.A., Banerjee, A.: Dynamic boundaries: Information hiding by second order framing with first order assertions. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 2\u201322. Springer, Heidelberg (2010)"},{"key":"13_CR21","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.tcs.2006.07.035","volume":"365","author":"D.A. Naumann","year":"2006","unstructured":"Naumann, D.A., Barnett, M.: Towards imperative modules: Reasoning about invariants and sharing of mutable state. Theoretical Comput. Sci.\u00a0365, 143\u2013168 (2006)","journal-title":"Theoretical Comput. Sci."},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 1. Springer, Heidelberg (2001)"},{"key":"13_CR23","unstructured":"Rosenberg, S., Banerjee, A., Naumann, D.A.: Verifier for region logic (VERL), http:\/\/www.cs.stevens.edu\/~naumann\/pub\/VERL\/"},{"key":"13_CR24","unstructured":"Shaner, S.M., Rajan, H., Leavens, G.T.: Model programs for preserving composite invariants. In: [18]"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009","author":"J. Smans","year":"2009","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol.\u00a05653, pp. 148\u2013172. Springer, Heidelberg (2009)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-78743-3_19","volume-title":"Fundamental Approaches to Software Engineering","author":"J. Smans","year":"2008","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for Java-like programs based on dynamic frames. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 261\u2013275. Springer, Heidelberg (2008)"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/978-3-642-11319-2_24","volume-title":"VMCAI 2010","author":"A.J. Summers","year":"2010","unstructured":"Summers, A.J., Drossopoulou, S.: Considerate reasoning and the composite design pattern. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 328\u2013344. 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-15057-9_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T03:01:00Z","timestamp":1606186860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}