{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T15:48:06Z","timestamp":1762271286750},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705918"},{"type":"electronic","value":"9783540705925"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70592-5_18","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"412-437","source":"Crossref","is-referenced-by-count":32,"title":["A Unified Framework for Verification Techniques for Object Invariants"],"prefix":"10.1007","author":[{"given":"S.","family":"Drossopoulou","sequence":"first","affiliation":[]},{"given":"A.","family":"Francalanza","sequence":"additional","affiliation":[]},{"given":"P.","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"A. J.","family":"Summers","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"18_CR1","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)","journal-title":"JOT"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"CASSIS","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: CASSIS. LNCS, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"18_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.: 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":"18_CR4","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/1328438.1328452","volume-title":"POPL","author":"W.-N. Chin","year":"2008","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL, pp. 87\u201399. ACM Press, New York (2008)"},{"key":"18_CR5","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1145\/286936.286947","volume-title":"OOPSLA","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA, vol.\u00a033(10), pp. 48\u201364. ACM Press, New York (1998)"},{"issue":"8","key":"18_CR6","doi-asserted-by":"crossref","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. JOT\u00a04(8), 5\u201332 (2005)","journal-title":"JOT"},{"key":"18_CR7","unstructured":"Drossopoulou, S., Francalanza, A., M\u00fcller, P.: A unified framework for verification techniques for object invariants. In: FOOL (2008)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/978-3-540-70592-5_18","volume-title":"ECOOP 2008","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: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 412\u2013437. Springer, Heidelberg (2008), http:\/\/www.doc.ic.ac.uk\/~ajs300m\/papers\/frameworkFull.pdf"},{"key":"18_CR9","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, pp. 337\u2013350. ACM Press, New York (2007)"},{"key":"18_CR10","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1145\/781131.781169","volume-title":"PLDI","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: A Type and Effect System for Atomicity. In: PLDI, pp. 338\u2013349. ACM Press, New York (2003)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-540-30569-9_8","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"R. H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 151\u2013171. Springer, Heidelberg (2005)"},{"key":"18_CR12","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":"10","key":"18_CR13","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"C.A.R. Hoare","year":"1974","unstructured":"Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM\u00a017(10), 549\u2013557 (1974)","journal-title":"Commun. ACM"},{"key":"18_CR14","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.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol.\u00a01783, pp. 208\u2013221. Springer, Heidelberg (2000)"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/360204.375719","volume-title":"POPL","author":"S.S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14\u201326. ACM Press, New York (2001)"},{"key":"18_CR16","first-page":"385","volume-title":"ICSE","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., M\u00fcller, P.: Information hiding and visibility in interface specifications. In: ICSE, pp. 385\u2013395. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"18_CR17","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Department of Computer Science, Iowa State University (February 2007), http:\/\/www.jmlspecs.org"},{"key":"18_CR18","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":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","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. 316\u2013330. Springer, Heidelberg (2007)"},{"key":"18_CR20","volume-title":"Abstraction and Specification in Program Development","author":"B. Liskov","year":"1986","unstructured":"Liskov, B., Guttag, J.: Abstraction and Specification in Program Development. MIT Press, Cambridge (1986)"},{"issue":"6","key":"18_CR21","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"B. Liskov","year":"1994","unstructured":"Liskov, B., Wing, J.: A behavioral notion of subtyping. ACM ToPLAS\u00a016(6), 1811\u20131841 (1994)","journal-title":"ACM ToPLAS"},{"key":"18_CR22","unstructured":"Lu, Y., Potter, J.: Soundness of Oval. Priv. Commun. (June 2007)"},{"key":"18_CR23","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.: Object Invariants and Effects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 202\u2013226. Springer, Heidelberg (2007)"},{"key":"18_CR24","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice-Hall, Englewood Cliffs (1988)"},{"key":"18_CR25","volume-title":"Eiffel: The Language","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Eiffel: The Language. Prentice-Hall, Englewood Cliffs (1992)"},{"key":"18_CR26","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/j.entcs.2007.08.034","volume":"195","author":"R. Middelkoop","year":"2008","unstructured":"Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.J.: Invariants for non-hierarchical object structures. Electr. Notes Theor. Comput. Sci.\u00a0195, 211\u2013229 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"18_CR27","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":"18_CR28","unstructured":"Parkinson, M.: Class invariants: the end of the road? In: International Workshop on Aliasing, Confinement and Ownership (2007)"},{"key":"18_CR29","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1145\/1040305.1040326","volume-title":"POPL","author":"M. Parkinson","year":"2005","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL, pp. 247\u2013258. ACM Press, New York (2005)"},{"key":"18_CR30","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/1328438.1328451","volume-title":"POPL","author":"M. Parkinson","year":"2008","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: POPL, pp. 75\u201386. ACM Press, New York (2008)"},{"key":"18_CR31","unstructured":"Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (1997)"},{"key":"18_CR32","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"18_CR33","first-page":"162","volume-title":"LICS","author":"J.P. Talpin","year":"1992","unstructured":"Talpin, J.P., Jouvelot, P.: The Type and Effect Discipline. In: LICS, pp. 162\u2013173. IEEE Computer Society Press, Los Alamitos (1992)"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2008 \u2013 Object-Oriented Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70592-5_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T14:51:06Z","timestamp":1684507866000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70592-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705918","9783540705925"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70592-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}