{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:28:35Z","timestamp":1725488915468},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735885"},{"type":"electronic","value":"9783540735892"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73589-2_11","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T21:48:05Z","timestamp":1186955285000},"page":"202-226","source":"Crossref","is-referenced-by-count":12,"title":["Validity Invariants and Effects"],"prefix":"10.1007","author":[{"given":"Yi","family":"Lu","sequence":"first","affiliation":[]},{"given":"John","family":"Potter","sequence":"additional","affiliation":[]},{"given":"Jingling","family":"Xue","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"J. Aldrich","year":"2004","unstructured":"Aldrich, J., Chambers, C.: Ownership domains: Separating aliasing policy from mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, Springer, Heidelberg (2004)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/BFb0053373","volume-title":"ECOOP \u201997 - Object-Oriented Programming","author":"P.S. Almeida","year":"1997","unstructured":"Almeida, P.S.: Balloon types: Controlling sharing of state in data types. In: Aksit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 32\u201359. Springer, Heidelberg (1997)"},{"issue":"6","key":"11_CR3","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., Fahndrich, M., Leino, K., 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":"11_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., Naumann, D.: Friends need a bit more: Maintaining invariants over shared state. In: Mathematics of Program Construction, pp. 54\u201384 (2004)","DOI":"10.1007\/978-3-540-27764-4_5"},{"key":"11_CR5","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1145\/1028976.1028980","volume-title":"OOPSLA \u201904","author":"A. Birka","year":"2004","unstructured":"Birka, A., Ernst, M.D.: A practical type system and language for reference immutability. In: OOPSLA \u201904. Proceedings of the 19th annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 35\u201349. ACM Press, New York (2004)"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Mathematics of Program Construction, pp. 102\u2013126 (2000)","DOI":"10.1007\/10722010_8"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT sysposium on Principles of programming languages, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/604131.604156","volume-title":"Proceedings of the 30th ACM 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: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 213\u2013223. ACM Press, New York (2003)"},{"key":"11_CR9","unstructured":"Clarke, D.: Object Ownership and Containment. PhD thesis, School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia (2001)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, D.G., Drossopoulou, S.: Ownership, encapsulation and disjointness of type and effect. In: 17th Annual Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (November 2002)","DOI":"10.1145\/582419.582447"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_4","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"D.G. Clarke","year":"2001","unstructured":"Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, Springer, Heidelberg (2001)"},{"key":"11_CR12","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/286936.286947","volume-title":"Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications","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 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 48\u201364. ACM Press, New York (1998)"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Dietl, W., Muller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology (JOT)\u00a0(2005)","DOI":"10.5381\/jot.2005.4.8.a1"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/117954.117975","volume-title":"OOPSLA \u201991","author":"J. Hogg","year":"1991","unstructured":"Hogg, J.: Islands: aliasing protection in object-oriented languages. In: OOPSLA \u201991. Proceedings of Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 271\u2013285. ACM Press, New York (1991)"},{"key":"11_CR15","volume-title":"Proceedings of the 28th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages","author":"S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: Bi as an assertion language for mutable data structures. In: Proceedings of the 28th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages, ACM Press, New York (2001)"},{"issue":"4","key":"11_CR16","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1109\/52.300040","volume":"8","author":"G. Leavens","year":"1991","unstructured":"Leavens, G.: Modular specification and verification of object-oriented programs. Software\u00a08(4), 72\u201380 (1991)","journal-title":"Software"},{"key":"11_CR17","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":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11785477_6","volume-title":"ECOOP 2006 \u2013 Object-Oriented Programming","author":"Y. Lu","year":"2006","unstructured":"Lu, Y., Potter, J.: On ownership and accessibility. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol.\u00a04067, pp. 99\u2013123. Springer, Heidelberg (2006)"},{"key":"11_CR19","volume-title":"Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Y. Lu","year":"2006","unstructured":"Lu, Y., Potter, J.: Protecting representation with effect encapsulation. In: Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York (2006)"},{"key":"11_CR20","volume-title":"Eiffel: the language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: the language. Prentice-Hall, Inc, Upper Saddle River, NJ, USA (1992)"},{"key":"11_CR21","volume-title":"Object-oriented software construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-oriented software construction, 2nd edn. Prentice-Hall, Upper Saddle River, NJ, USA (1997)","edition":"2"},{"key":"11_CR22","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":"11_CR23","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: Universes: A type system for controlling representation exposure. In: Programming Languages and Fundamentals of Programming (1999)"},{"key":"11_CR24","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: Universes: A Type System for Alias and Dependency Control. Fernuniv. Fachbereich Informatik (2001)"},{"key":"11_CR25","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversit\u00e4t Hagen (2001)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Muller, P., Poetzsch-Heffter, A., Leavens, G.: Modular invariants for layered object structures. Science of Computer Programming (2006)","DOI":"10.1016\/j.scico.2006.03.001"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Naumann, D., Barnett, M.: Towards imperative modules: reasoning about invariants and sharing of mutable state. In: Logic in Computer Science, 2004. Proceedings of the 19th Annual IEEE Symposium, pp. 313\u2013323 (2004)","DOI":"10.1109\/LICS.2004.1319626"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP \u201998 - Object-Oriented Programming","author":"J. Noble","year":"1998","unstructured":"Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol.\u00a01445, Springer, Heidelberg (1998)"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: 2002. Proceedings. 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"11_CR30","unstructured":"Schulte, W.: Towards a Verifying Compiler: The Spec# Approach. Microsoft Research (2006), http:\/\/research.microsoft.com\/specsharp\/"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2007 \u2013 Object-Oriented Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73589-2_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:52:42Z","timestamp":1619517162000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73589-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735885","9783540735892"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73589-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}