{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T23:02:24Z","timestamp":1767999744984,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319064093","type":"print"},{"value":"9783319064109","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_35","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T21:03:01Z","timestamp":1397854981000},"page":"514-530","source":"Crossref","is-referenced-by-count":22,"title":["Flexible Invariants through Semantic Collaboration"],"prefix":"10.1007","author":[{"given":"Nadia","family":"Polikarpova","sequence":"first","affiliation":[]},{"given":"Julian","family":"Tschannen","sequence":"additional","affiliation":[]},{"given":"Carlo A.","family":"Furia","sequence":"additional","affiliation":[]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","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)"},{"issue":"6","key":"35_CR2","doi-asserted-by":"crossref","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"Mike Barnett","year":"2004","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)","journal-title":"The Journal of Object Technology"},{"issue":"6","key":"35_CR3","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M. Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. Commun. ACM\u00a054(6), 81\u201391 (2011)","journal-title":"Commun. ACM"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-642-14295-6_42","volume-title":"Computer Aided Verification","author":"E. Cohen","year":"2010","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local verification of global invariants in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 480\u2013494. Springer, Heidelberg (2010)"},{"key":"35_CR6","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns. Addison-Wesley (1994)"},{"key":"35_CR7","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":"Gary T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175\u2013188 (1999)"},{"issue":"2","key":"35_CR8","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Asp. Comput.\u00a019(2), 159\u2013189 (2007)","journal-title":"Formal Asp. Comput."},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-642-05089-3_51","volume-title":"FM 2009: Formal Methods","author":"D. Leinenbach","year":"2009","unstructured":"Leinenbach, D., Santen, T.: Verifying the Microsoft Hyper-V Hypervisor with VCC. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 806\u2013809. Springer, Heidelberg (2009)"},{"key":"35_CR10","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":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","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. 80\u201394. Springer, Heidelberg (2007)"},{"key":"35_CR12","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall (1997)"},{"key":"35_CR13","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/j.entcs.2006.05.025","volume":"160","author":"R. Middelkoop","year":"2006","unstructured":"Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.J.: Cooperation-based invariants for OO languages. Electr. Notes Theor. Comput. Sci.\u00a0160, 225\u2013237 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"35_CR14","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."},{"issue":"3","key":"35_CR15","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":"35_CR16","unstructured":"Parkinson, M.J.: Class invariants: the end of the road? In: IWACO. ACM (2007)"},{"key":"35_CR17","unstructured":"SAVCBS workshop series (2001-2010), http:\/\/www.eecs.ucf.edu\/~leavens\/SAVCBS\/"},{"key":"35_CR18","unstructured":"Semantic Collaboration website, http:\/\/se.inf.ethz.ch\/people\/polikarpova\/sc\/"},{"issue":"9","key":"35_CR19","doi-asserted-by":"publisher","first-page":"1175","DOI":"10.1109\/12.57058","volume":"39","author":"L. Sha","year":"1990","unstructured":"Sha, L., Rajkumar, R., Lehoczky, J.P.: Priority inheritance protocols: An approach to real-time synchronization. IEEE Trans. Comput.\u00a039(9), 1175\u20131185 (1990)","journal-title":"IEEE Trans. Comput."},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-642-11319-2_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.J. Summers","year":"2010","unstructured":"Summers, A.J., Drossopoulou, S.: Considerate reasoning and the composite design pattern. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 328\u2013344. Springer, Heidelberg (2010)"},{"key":"35_CR21","doi-asserted-by":"crossref","unstructured":"Summers, A.J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: IWACO, pp. 1\u20139. ACM (2009)","DOI":"10.1145\/1562154.1562160"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T17:44:51Z","timestamp":1565372691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}