{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:21Z","timestamp":1725516501852},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_12","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"93-104","source":"Crossref","is-referenced-by-count":1,"title":["Reasoning about Object Structures Using Ownership"],"prefix":"10.1007","author":[{"given":"Peter","family":"M\u00fcller","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/BFb0030634","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"M. Abadi","year":"1997","unstructured":"Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 682\u2013696. Springer, Heidelberg (1997)"},{"key":"12_CR2","first-page":"166","volume-title":"Principles of Programming Languages","author":"A. Banerjee","year":"2002","unstructured":"Banerjee, A., Naumann, D.: Representation independence, confinement, and access control. In: Principles of Programming Languages, pp. 166\u2013177. ACM Press, New York (2002)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Submitted (2006), http:\/\/research.microsoft.com\/~leino\/papers\/krml160.pdf","DOI":"10.1007\/11804192_17"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2004)"},{"key":"12_CR5","first-page":"211","volume-title":"Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 211\u2013230. ACM Press, New York (2002)"},{"key":"12_CR6","series-title":"SIGPLAN Notices","volume-title":"Proceedings of Object-Oriented Programming Systems, Languages, and Applications (OOPSLA)","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: Proceedings of Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), October 1998. SIGPLAN Notices, vol.\u00a033(10), ACM Press, New York (1998)"},{"key":"12_CR7","first-page":"238","volume-title":"Principles of programming languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of programming languages (POPL), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Darvas, A., M\u00fcller, P.: Reasoning About Method Calls in Interface Specifications. Journal of Object Technology (JOT) (to appear, 2006)","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"12_CR9","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (July 2003)"},{"key":"12_CR10","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G.: Wrestling with rep exposure. Research Report 156, Digital Systems Research Center (1998)"},{"key":"12_CR11","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Digital Systems Research Center (1998)"},{"issue":"8","key":"12_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/jot.2005.4.8.a1","volume":"4","author":"W. Dietl","year":"2005","unstructured":"Dietl, W., M\u00fcller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT)\u00a04(8), 5\u201332 (2005)","journal-title":"Journal of Object Technology (JOT)"},{"issue":"2","key":"12_CR13","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":"12_CR14","first-page":"302","volume-title":"Object-oriented programing, systems, languages, and applications (OOPSLA)","author":"M. F\u00e4hndrich","year":"2003","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Object-oriented programing, systems, languages, and applications (OOPSLA), pp. 302\u2013312. ACM Press, New York (2003)"},{"key":"12_CR15","first-page":"234","volume-title":"Programming Language Design and Implementation (PLDI)","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI), pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"12_CR16","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 representation. Acta Informatica\u00a01, 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"issue":"1","key":"12_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. Journal of the ACM\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the ACM"},{"key":"12_CR18","unstructured":"Jacobs, B., Leino, K.R.M., Schulte, W.: Verification of multithreaded object-oriented programs with invariants. In: Specification and Verification of Component-Based Systems (SAVCBS), pp. 2\u20139, Technical report 04-09, Department of Computer Science, Iowa State University (2004)"},{"key":"12_CR19","doi-asserted-by":"publisher","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":"12_CR20","series-title":"SIGPLAN","first-page":"212","volume-title":"OOPSLA ECOOP 1990 Proceedings","author":"G.T. Leavens","year":"1990","unstructured":"Leavens, G.T., Weihl, W.E.: Reasoning about object-oriented programs that use subtypes (extended abstract). In: Meyrowitz, N. (ed.) OOPSLA ECOOP 1990 Proceedings. SIGPLAN, vol.\u00a025(10), pp. 212\u2013223. ACM Press, New York (1990)"},{"key":"12_CR21","unstructured":"Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology (1995)"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/11526841_4","volume-title":"FM 2005: Formal Methods","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., M\u00fcller, P.: Modular verification of static class invariants. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 26\u201342. Springer, Heidelberg (2005)"},{"issue":"5","key":"12_CR24","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 Transactions on Programming Languages and Systems\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"volume-title":"Abstraction and Specification in Program Development","year":"1986","author":"B. Liskov","key":"12_CR25","unstructured":"Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)"},{"key":"12_CR26","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":"12_CR27","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":"12_CR28","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. LNCS, vol.\u00a02262. Springer, Heidelberg (2002)"},{"key":"12_CR29","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"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. In: Science of Computer Programming, ETH Zurich. Accepted for publication. Also available as TR\u00a0424 of the Department of Computer Science (2006)","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-30579-8_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Salcianu","year":"2005","unstructured":"Salcianu, A., Rinard, M.: Purity and side effect analysis for java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 199\u2013215. Springer, Heidelberg (2005)"}],"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-540-69149-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:42:39Z","timestamp":1557718959000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}