{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:53:45Z","timestamp":1762458825911},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221593"},{"type":"electronic","value":"9783540248514"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24851-4_22","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:36:03Z","timestamp":1281299763000},"page":"491-515","source":"Crossref","is-referenced-by-count":117,"title":["Object Invariants in Dynamic Contexts"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. Manuscript available on (December 2002), \n                    \n                      http:\/\/guinness.cs.stevens-tech.edu\/~naumann\/publications\/"},{"key":"22_CR2","doi-asserted-by":"crossref","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 (2004) (to appear)","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: 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":"22_CR4","series-title":"SIGPLAN Notices","first-page":"82","volume-title":"Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 1999)","author":"B. Bokowski","year":"1999","unstructured":"Bokowski, B., Vitek, J.: Confined types. In: Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 1999), October 1999. SIGPLAN Notices, vol.\u00a034(10), pp. 82\u201396. ACM, New York (1999)"},{"key":"22_CR5","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/582419.582440","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, November 2002. SIGPLAN Notices, vol.\u00a037(11), pp. 211\u2013230. ACM, New York (2002)"},{"key":"22_CR6","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/604131.604156","volume-title":"Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"C. Boyapati","year":"2003","unstructured":"Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2003. SIGPLAN Notices, vol.\u00a038(1), pp. 213\u2013223. ACM, New York (2003)"},{"key":"22_CR7","unstructured":"Clarke, D.: Object Ownership and Containment. PhD thesis, University of New South Wales (2001)"},{"key":"22_CR8","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/582419.582447","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002","author":"D.G. Clarke","year":"2002","unstructured":"Clarke, D.G., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, November 2002. SIGPLAN Notices, vol.\u00a037(11), pp. 292\u2013310. ACM, New York (2002)"},{"key":"22_CR9","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/286936.286947","volume-title":"Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 1998)","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 1998), October 1998. SIGPLAN Notices, vol.\u00a033(10), pp. 48\u201364. ACM, New York (1998)"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-45070-2_9","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"D.G. Clarke","year":"2003","unstructured":"Clarke, D.G., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 176\u2013200. Springer, Heidelberg (2003)"},{"key":"22_CR11","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G.: Wrestling with rep exposure. Research Report 156, Digital Equipment Corporation Systems Research Center (July 1998)"},{"key":"22_CR12","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (December 1998)"},{"key":"22_CR13","unstructured":"Dhara, K.K.: Behavioral subtyping in object-oriented languages. Technical Report 97-09, Iowa State University (May 1997)"},{"issue":"2","key":"22_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/32.908957","volume":"27","author":"M.D. Ernst","year":"2001","unstructured":"Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering\u00a027(2), 1\u201325 (2001)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"22_CR15","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/512529.512532","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"M. F\u00e4hndrich","year":"2002","unstructured":"F\u00e4hndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), May 2002. SIGPLAN Notices, vol.\u00a037(5), pp. 13\u201324. ACM, New York (2002)"},{"key":"22_CR16","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Rustan, K., Leino, M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), May 2002. SIGPLAN Notices, vol.\u00a037(5), pp. 234\u2013245. ACM, New York (2002)"},{"key":"22_CR17","series-title":"Texts and Monographs in Computer Science","volume-title":"Larch: Languages and Tools for Formal Specification","year":"1993","unstructured":"Guttag, J.V., Horning, J.J. (eds.): Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer, Heidelberg (1993); With Stephen J. Garland, Kevin D. Jones, Andr\u00e9s Modet, and Jeannette M.Wing"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-46428-X_15","volume-title":"Fundamental Approaches to Software Engineering","author":"K. Huizing","year":"2000","unstructured":"Huizing, K., Kuiper, R.: Verification of object-oriented programs using class invariants. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 208\u2013221. Springer, Heidelberg (2000)"},{"key":"22_CR19","unstructured":"Joshi, R.: Extended static checking of programs with cyclic dependencies. In: Mason, J. (ed.) 1997 SRC Summer Intern Projects, Technical Note 1997-028. Digital Equipment Corporation Systems Research Center (1997)"},{"key":"22_CR20","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"22_CR21","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML:A behavioral interface specification language for Java. Technical Report 98-06v, Iowa State University, Department of Computer Science (May 2003), See \n                    \n                      http:\/\/www.jmlspecs.org"},{"key":"22_CR22","volume-title":"Foundations of Component-Based Systems","author":"G.T. Leavens","year":"2000","unstructured":"Leavens, G.T., Dhara, K.K.: Concepts of behavioral subtyping and a sketch of their extension to component-based systems. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, Cambridge University Press, Cambridge (2000)"},{"key":"22_CR23","unstructured":"Rustan, K., Leino, M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology (1995)"},{"issue":"5","key":"22_CR24","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K. Rustan","year":"2002","unstructured":"Rustan, K., Leino, M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR25","unstructured":"Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: ESC\/Java user\u2019s manual. Technical Note 2000-002, Compaq Systems Research Center (October 2000)"},{"key":"22_CR26","series-title":"Electrical Engineering and Computer Science Series. MIT Press","volume-title":"Abstraction and Specification in Program Development","author":"B. Liskov","year":"1986","unstructured":"Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. Electrical Engineering and Computer Science Series. MIT Press. MIT Press, Cambridge (1986)"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems\u00a016(6) (1994)","DOI":"10.1145\/197320.197383"},{"key":"22_CR28","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"22_CR29","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. LNCS, vol.\u00a02262. Springer, Heidelberg (2002); PhD thesis, FernUniversit\u00e4t Hagen"},{"key":"22_CR31","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, FernUniversit\u00e4t Hagen (2001)"},{"key":"22_CR32","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Technical Report 424, Department of Computer Science, ETH Zurich (2003)"},{"key":"22_CR33","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1002\/cpe.713","volume":"15","author":"P. M\u00fcller","year":"2003","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurrency and Computation: Practice and Experience\u00a015, 117\u2013154 (2003)","journal-title":"Concurrency and Computation: Practice and Experience"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2004 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24851-4_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:15:19Z","timestamp":1620011719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24851-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221593","9783540248514"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24851-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}