{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T12:26:20Z","timestamp":1725798380414},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319104300"},{"type":"electronic","value":"9783319104317"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10431-7_25","type":"book-chapter","created":{"date-parts":[[2014,8,4]],"date-time":"2014-08-04T05:27:28Z","timestamp":1407130048000},"page":"302-316","source":"Crossref","is-referenced-by-count":2,"title":["More Flexible Object Invariants with Less Specification Overhead"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Huster","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Heckeler","sequence":"additional","affiliation":[]},{"given":"Hanno","family":"Eichelberger","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Ruf","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Burg","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Rosenstiel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Summers, A.J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming, pp. 1\u20139. ACM (2009)","DOI":"10.1145\/1562154.1562160"},{"key":"25_CR2","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\u2013515. Springer, Heidelberg (2004)"},{"key":"25_CR3","unstructured":"Barnett, M., F\u00e4hndrich, M., M\u00fcller, P., Leino, K.R.M., Schulte, W., Venter, H.: Specification and verification: The spec# experience (2009)"},{"issue":"10","key":"25_CR4","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"issue":"3","key":"25_CR5","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. Sci. Comput. Program.\u00a062(3), 253\u2013286 (2006)","journal-title":"Sci. Comput. Program."},{"key":"25_CR6","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall, Inc., Upper Saddle River (1992)"},{"key":"25_CR7","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Jml: a java modeling language. In: Formal Underpinnings of Java Workshop, at OOPSLA 1998 (1998)"},{"key":"25_CR8","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":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-36946-9_11","volume-title":"Aliasing in Object-Oriented Programming. Types, Analysis and Verification","author":"W. Dietl","year":"2013","unstructured":"Dietl, W., M\u00fcller, P.: Object ownership in program verification. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol.\u00a07850, pp. 289\u2013318. Springer, Heidelberg (2013)"},{"key":"25_CR10","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":"25_CR11","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P.: Reasoning about object structures using ownership. In: Meyer, B., Woodcock, J. (eds.) Verified Software. LNCS, vol.\u00a04171, pp. 93\u2013104. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-69149-5_12"},{"key":"25_CR12","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.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":"25_CR13","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":"25_CR14","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\u00a03, 2004 (2004)","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"25_CR15","first-page":"385","volume-title":"Proceedings of the 29th International Conference on Software Engineering, ICSE 2007","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Muller, P.: Information hiding and visibility in interface specifications. In: Proceedings of the 29th International Conference on Software Engineering, ICSE 2007, pp. 385\u2013395. IEEE Computer Society, Washington, DC (2007)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10431-7_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T09:17:47Z","timestamp":1558948667000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10431-7_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319104300","9783319104317"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10431-7_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}