{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:52:45Z","timestamp":1725519165812},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540878728"},{"type":"electronic","value":"9783540878735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87873-5_17","type":"book-chapter","created":{"date-parts":[[2008,9,25]],"date-time":"2008-09-25T12:04:10Z","timestamp":1222344250000},"page":"192-208","source":"Crossref","is-referenced-by-count":22,"title":["Flexible Immutability with Frozen Objects"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Angela","family":"Wallenburg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","first-page":"311","volume-title":"OOPSLA","author":"J. Aldrich","year":"2002","unstructured":"Aldrich, J., Kostadinov, V., Chambers, C.: Alias annotations for program understanding. In: OOPSLA, pp. 311\u2013330. ACM Press, New York (2002)"},{"issue":"6","key":"17_CR2","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. JOT\u00a03(6), 27\u201356 (2004), www.jot.fm","journal-title":"JOT"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 54\u201384. Springer, Heidelberg (2004)"},{"key":"17_CR4","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/1040305.1040327","volume-title":"POPL","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, vol.\u00a040(1), pp. 259\u2013270. ACM, New York (2005)"},{"key":"17_CR5","unstructured":"Boyapati, C.: SafeJava: A Unified Type System for Safe Programming. Ph.D., MIT (2004)"},{"key":"17_CR6","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)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/978-3-540-45070-2_9","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"D. Clarke","year":"2003","unstructured":"Clarke, D., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 176\u2013200. Springer, Heidelberg (2003)"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA. ACM SIGPLAN Notices, vol.\u00a033(10) (1998)","DOI":"10.1145\/286936.286947"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-71289-3_26","volume-title":"Fundamental Approaches to Software Engineering","author":"\u00c1. Darvas","year":"2007","unstructured":"Darvas, \u00c1., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol.\u00a04422, pp. 336\u2013351. Springer, Heidelberg (2007)"},{"issue":"5","key":"17_CR10","doi-asserted-by":"crossref","first-page":"59","DOI":"10.5381\/jot.2006.5.5.a3","volume":"5","author":"\u00c1. Darvas","year":"2006","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning about method calls in interface specifications. JOT\u00a05(5), 59\u201385 (2006)","journal-title":"JOT"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-78739-6","volume-title":"ECOOP","author":"S. Drossopoulou","year":"2008","unstructured":"Drossopoulou, S., Francalanza, A., M\u00fcller, P., Summers, A.J.: A unified framework for verification techniques for object invariants. In: ECOOP. LNCS. Springer, Heidelberg (2008)"},{"key":"17_CR12","series-title":"SIGPLAN Notices","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1145\/1297027.1297052","volume-title":"OOPSLA","author":"M. F\u00e4hndrich","year":"2007","unstructured":"F\u00e4hndrich, M., Xia, S.: Establishing object invariants with delayed types. In: OOPSLA. SIGPLAN Notices, vol.\u00a042(10), pp. 337\u2013350. ACM, New York (2007)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-71316-6_24","volume-title":"Programming Languages and Systems","author":"C. Haack","year":"2007","unstructured":"Haack, C., Poll, E., Sch\u00e4fer, J., Schubert, A.: Immutable objects for a Java-like language. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 347\u2013362. Springer, Heidelberg (2007)"},{"key":"17_CR14","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)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-78739-6_24","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2008","unstructured":"Leino, K.R.M., M\u00fcller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 307\u2013321. Springer, Heidelberg (2008)"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-540-71316-6_7","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2007","unstructured":"Leino, K.R.M., Schulte, W.: Using history invariants to verify observers. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 80\u201394. Springer, Heidelberg (2007)"},{"key":"17_CR17","volume-title":"First India Software Engineering Conference (ISEC)","author":"K.R.M. Leino","year":"2008","unstructured":"Leino, K.R.M., Wallenburg, A.: Class-local object invariants. In: First India Software Engineering Conference (ISEC). ACM, New York (2008)"},{"key":"17_CR18","unstructured":"Liskov, B., Curtis, D., Day, M., Ghemawat, S., Gruber, R., Johnson, P., Myers, A.C.: Theta reference manual, preliminary version. Memo\u00a088, Programming Methodology Group, MIT Laboratory for Computer Science (1995), http:\/\/www.pmg.lcs.mit.edu\/Theta.html"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-73589-2_11","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"Y. Lu","year":"2007","unstructured":"Lu, Y., Potter, J., Xue, J.: Validity invariants and effects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 202\u2013226. Springer, Heidelberg (2007)"},{"key":"17_CR20","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. Science of Computer Programming\u00a062, 253\u2013286 (2006)","journal-title":"Science of Computer Programming"},{"key":"17_CR21","series-title":"SIGPLAN Notices","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1145\/1297027.1297061","volume-title":"OOPSLA","author":"P. M\u00fcller","year":"2007","unstructured":"M\u00fcller, P., Rudich, A.: Ownership transfer in Universe Types. In: OOPSLA. SIGPLAN Notices, vol.\u00a042(10), pp. 461\u2013478. ACM, New York (2007)"},{"issue":"3","key":"17_CR22","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/j.tcs.2007.02.004","volume":"376","author":"D.A. Naumann","year":"2007","unstructured":"Naumann, D.A.: Observational purity and encapsulation. TCS\u00a0376(3), 205\u2013224 (2007)","journal-title":"TCS"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"\u00d6stlund, J., Wrigstad, T., Clarke, D., \u00c5kerblom, B.: Ownership, uniqueness and immutability. In: IWACO (2007)","DOI":"10.1007\/978-3-540-69824-1_11"},{"key":"17_CR24","series-title":"SIGPLAN Notices","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1145\/1094811.1094828","volume-title":"OOPSLA","author":"M.S. Tschantz","year":"2005","unstructured":"Tschantz, M.S., Ernst, M.D.: Javari: adding reference immutability to Java. In: OOPSLA. SIGPLAN Notices, vol.\u00a040(10), pp. 211\u2013230. ACM, New York (2005)"},{"key":"17_CR25","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/1287624.1287637","volume-title":"ESEC-FSE","author":"Y. Zibin","year":"2007","unstructured":"Zibin, Y., Potanin, A., Ali, M., Artzi, S., Kie\u017cun, A., Ernst, M.D.: Object and reference immutability using java generics. In: ESEC-FSE, pp. 75\u201384. ACM, New York (2007)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87873-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,20]],"date-time":"2023-05-20T02:27:24Z","timestamp":1684549644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87873-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540878728","9783540878735"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87873-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}