{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:24:20Z","timestamp":1760783060386},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705918"},{"type":"electronic","value":"9783540705925"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70592-5_17","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"387-411","source":"Crossref","is-referenced-by-count":56,"title":["Regional Logic for Local Reasoning about Global Invariants"],"prefix":"10.1007","author":[{"given":"Anindya","family":"Banerjee","sequence":"first","affiliation":[]},{"given":"David A.","family":"Naumann","sequence":"additional","affiliation":[]},{"given":"Stan","family":"Rosenberg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: ACM Symposium on Principles of Programming Languages (POPL) (2006)","DOI":"10.1145\/1111037.1111046"},{"issue":"6","key":"17_CR2","doi-asserted-by":"publisher","first-page":"894","DOI":"10.1145\/1101821.1101824","volume":"52","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Journal of the ACM\u00a052(6), 894\u2013960 (2005)","journal-title":"Journal of the ACM"},{"key":"17_CR3","unstructured":"Banerjee, A., Naumann, D., Rosenberg, S.: Regional logic for local reasoning about global invariants, www.cs.stevens.edu\/~naumann\/pub\/rllrgi.pdf"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Banerjee, A., Naumann, D., Rosenberg, S.: Towards a logical account of declassification. In: ACM Workshop on Programming Languages and Analysis for Security (2007)","DOI":"10.1145\/1255329.1255340"},{"issue":"6","key":"17_CR5","doi-asserted-by":"crossref","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Bierman, G., Parkinson, M.: Separation logic and abstraction. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 247\u2013258 (2005)","DOI":"10.1145\/1047659.1040326"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: IEEE Symp. on Logic in Computer Science (LICS) (2005)","DOI":"10.1109\/LICS.2005.47"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: MPC (2000)","DOI":"10.1007\/10722010_8"},{"issue":"3","key":"17_CR9","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/S0304-3975(02)00868-X","volume":"298","author":"C. Calcagno","year":"2003","unstructured":"Calcagno, C., O\u2019Hearn, P., Bornat, R.: Program logic and equivalence in the presence of garbage collection. Theoretical Comput. Sci.\u00a0298(3), 557\u2013581 (2003)","journal-title":"Theoretical Comput. Sci."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Cameron, N.R., Drossopoulou, S., Noble, J., Smith, M.J.: Multiple ownership. In: OOPSLA (2007)","DOI":"10.1145\/1297027.1297060"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA, pp. 292\u2013310 (November 2002)","DOI":"10.1145\/582419.582447"},{"key":"17_CR12","unstructured":"Drossopoulou, S., Francalana, A., M\u00fcller, P.: A unified framework for verification techniques for object invariants. In: FOOL (2008)"},{"key":"17_CR13","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":"17_CR14","doi-asserted-by":"crossref","unstructured":"Kassios, I.T.: Dynamic framing: Support for framing, dependencies and sharing without restriction. In: Formal Methods: International Conference of Formal Methods Europe (2006)","DOI":"10.1007\/11813040_19"},{"key":"17_CR15","unstructured":"Leavens, G.T., Naumann, D.A., Rosenberg, S.: Preliminary definition of core JML. Technical Report CS Report 2006-07, Stevens Institute of Technology (2006)"},{"key":"17_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\u2013516. Springer, Heidelberg (2004)"},{"issue":"5","key":"17_CR17","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Trans. Prog. Lang. Syst.\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45651-1","volume-title":"Modular Specification and Verification of Object-Oriented Programs","author":"P. M\u00fcller","year":"2002","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. In: M\u00fcller, P. (ed.) Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262. Springer, Heidelberg (2002)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Rudich, A.: Ownership transfer in Universe Types. In: ACM Conf. on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA) (2007)","DOI":"10.1145\/1297027.1297061"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: ICFP (2006)","DOI":"10.1145\/1159803.1159812"},{"key":"17_CR21","unstructured":"Naumann, D.A.: An admissible second order frame rule in region logic. Technical Report CS Report 2008-02, Stevens Institute of Technology (2008)"},{"key":"17_CR22","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":"17_CR23","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"key":"17_CR24","unstructured":"Parkinson, M.: Class invariants: the end of the road. In: International Workshop on Aliasing, Confinement and Ownership (2007)"},{"key":"17_CR25","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1016\/j.tcs.2005.06.018","volume":"343","author":"C. Pierik","year":"2005","unstructured":"Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theoretical Comput. Sci.\u00a0343, 413\u2013442 (2005)","journal-title":"Theoretical Comput. Sci."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for java-like programs based on dynamic frames. In: FASE (2008)","DOI":"10.1007\/978-3-540-78743-3_19"},{"key":"17_CR27","unstructured":"Smith, M., Drossopoulou, S.: Cheaper reasoning with ownership types. In: International Workshop on Aliasing, Confinement and Ownership (2003)"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Tofte, M., Talpin, J.-P.: Implementation of the Typed Call-by-Value lambda-Calculus using a Stack of Regions. In: POPL (1994)","DOI":"10.1145\/174675.177855"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2008 \u2013 Object-Oriented Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70592-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:08:24Z","timestamp":1605762504000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70592-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705918","9783540705925"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70592-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}