{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:10:13Z","timestamp":1746159013429,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548031"},{"type":"electronic","value":"9783642548048"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54804-8_16","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:59:16Z","timestamp":1395395956000},"page":"230-245","source":"Crossref","is-referenced-by-count":6,"title":["Verifying Class Invariants in Concurrent Programs"],"prefix":"10.1007","author":[{"given":"Marina","family":"Zaharieva-Stojanovski","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Amighi, A., Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: The VerCors project: setting up basecamp. In: PLPV, pp. 71\u201382 (2012)","DOI":"10.1145\/2103776.2103785"},{"issue":"4","key":"16_CR2","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1002\/stvr.281","volume":"13","author":"C. Artho","year":"2003","unstructured":"Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test., Verif. Reliab.\u00a013(4), 207\u2013227 (2003)","journal-title":"Softw. Test., Verif. Reliab."},{"issue":"6","key":"16_CR3","doi-asserted-by":"publisher","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. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 259\u2013270. ACM (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"16_CR5","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":"16_CR6","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)"},{"issue":"8","key":"16_CR7","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\u00a04(8), 5\u201332 (2005)","journal-title":"Journal of Object Technology"},{"key":"16_CR8","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":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-70592-5_18","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","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)"},{"issue":"1-3","key":"16_CR10","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2004.12.006","volume":"338","author":"C. Flanagan","year":"2005","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci.\u00a0338(1-3), 153\u2013183 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR11","unstructured":"Haack, C., Huisman, M., Hurlin, C., Amighi, A.: Permission-based separation logic for Java, 201x. Conditionally accepted for LMCS"},{"issue":"10","key":"16_CR12","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. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"16_CR13","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":"16_CR14","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F., Leino, K.R.M., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: SEFM, pp. 137\u2013147 (2005)","DOI":"10.1109\/SEFM.2005.39"},{"key":"16_CR15","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)"},{"key":"16_CR16","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., Xue, J.: Validity invariants and effects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 202\u2013226. Springer, Heidelberg (2007)"},{"key":"16_CR17","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall (1997)"},{"issue":"3","key":"16_CR18","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."},{"issue":"1-3","key":"16_CR19","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: Principles of programming languages (POPL 2008), pp. 75\u201386. ACM (2008)","DOI":"10.1145\/1328897.1328451"},{"key":"16_CR21","unstructured":"Parkinson, M.J.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge, Computer Laboratory (November 2005)"},{"key":"16_CR22","unstructured":"Poetzsch-Heffter, A.: Specification and Verification of Object-Oriented Programs. PhD thesis, Habilitation thesis, Technical University of Munich (1997)"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on LICS 2002, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"16_CR24","unstructured":"Wei\u00df, B.: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis, Karlsruhe Institute of Technology (2011)"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Zaharieva-Stojanovski, M., Huisman, M.: Verifying class invariants in concurrent programs. Technical Report TR-CTIT-13-10, Centre for Telematics and Information Technology, University of Twente (2014)","DOI":"10.1007\/978-3-642-54804-8_16"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54804-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T03:45:59Z","timestamp":1746157559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54804-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548031","9783642548048"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54804-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}