{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T19:10:01Z","timestamp":1739041801805,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005923"},{"type":"electronic","value":"9783642005930"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00593-0_16","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T10:26:08Z","timestamp":1238149568000},"page":"231-245","source":"Crossref","is-referenced-by-count":9,"title":["Proving Consistency of Pure Methods and Model Fields"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]},{"given":"Ronald","family":"Middelkoop","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"8","key":"16_CR1","doi-asserted-by":"publisher","first-page":"77","DOI":"10.5381\/jot.2005.4.8.a4","volume":"4","author":"D.R. Cok","year":"2005","unstructured":"Cok, D.R.: Reasoning with specifications containing method calls and model fields. Journal of Object Technology\u00a04(8), 77\u2013103 (2005) (FTfJP 2004 Special Issue)","journal-title":"Journal of Object Technology"},{"issue":"6","key":"16_CR2","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract. Softw. Pract. Exper.\u00a035(6), 583\u2013599 (2005)","journal-title":"Softw. Pract. Exper."},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-71289-3_26","volume-title":"Fundamental Approaches to Software Engineering","author":"\u00c1. Darvas","year":"2007","unstructured":"Darvas, \u00c1., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol.\u00a04422, pp. 336\u2013351. Springer, Heidelberg (2007)"},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"59","DOI":"10.5381\/jot.2006.5.5.a3","volume":"5","author":"\u00c1. Darvas","year":"2006","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning About Method Calls in Interface Specifications. Journal of Object Technology\u00a05(5), 59\u201385 (2006) (FTfJP 2005 Special Issue)","journal-title":"Journal of Object Technology"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11693024_9","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2006","unstructured":"Leino, K.R.M., M\u00fcller, P.: A verification methodology for model fields. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 115\u2013130. Springer, Heidelberg (2006)"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Middelkoop, R.: Proving consistency of pure methods and model fields. Technical report, Microsoft Research (2009)","DOI":"10.1007\/978-3-642-00593-0_16"},{"key":"16_CR9","unstructured":"Clarke, D.: Object Ownership and Containment. PhD thesis, University of New South Wales (2001)"},{"key":"16_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)"},{"issue":"6","key":"16_CR11","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) (FTfJP 2003 Special Issue)","journal-title":"Journal of Object Technology"},{"key":"16_CR12","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)"},{"issue":"1-4","key":"16_CR13","doi-asserted-by":"crossref","first-page":"377","DOI":"10.3233\/FUN-2008-851-426","volume":"85","author":"R. Middelkoop","year":"2008","unstructured":"Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.J.: Specification and Verification of Invariants by Exploiting Layers in OO Designs. Fundamenta Informaticae\u00a085(1-4), 377\u2013398 (2008) (CS&P 2007 Special Issue)","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"16_CR14","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(3), 253\u2013286 (2006)","journal-title":"Science of Computer Programming"},{"key":"16_CR15","first-page":"48","volume-title":"OOPSLA 1998","author":"D.G. Clarke","year":"1998","unstructured":"Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48\u201364. ACM Press, New York (1998)"},{"key":"16_CR16","first-page":"302","volume-title":"OOPSLA","author":"M. F\u00e4hndrich","year":"2003","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA, pp. 302\u2013312. ACM, New York (2003)"},{"key":"16_CR17","unstructured":"Breunesse, C.B., Poll, E.: Verifying JML specifications with model fields. In: FTfJP 2003, Technical Report 408, ETH Zurich, 51\u201360 (2003)"},{"issue":"2","key":"16_CR18","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/s00165-006-0016-1","volume":"19","author":"P. Chalin","year":"2007","unstructured":"Chalin, P.: Are the logical foundations of verifying compiler prototypes matching user expectations? Form. Asp. Comput.\u00a019(2), 139\u2013158 (2007)","journal-title":"Form. Asp. Comput."},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-68237-0_7","volume-title":"FM 2008: Formal Methods","author":"A. Rudich","year":"2008","unstructured":"Rudich, A., Darvas, \u00c1., M\u00fcller, P.: Checking well-formedness of pure-method specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 68\u201383. Springer, Heidelberg (2008)"},{"issue":"3","key":"16_CR20","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/j.tcs.2007.02.004","volume":"376","author":"D.A. Naumann","year":"2007","unstructured":"Naumann, D.A.: Observational purity and encapsulation. Theor. Comput. Sci.\u00a0376(3), 205\u2013224 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR21","unstructured":"Barnett, M., Naumann, D.A., Schulte, W., Sun, Q.: 99.44% pure: Useful abstractions in specifications. In: FTfJP 2004, Technical Report NIII-R0426, University of Nijmegen, 11\u201318 (2004)"},{"key":"16_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-78739-6_24","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2008","unstructured":"Leino, K.R.M., M\u00fcller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 307\u2013321. Springer, Heidelberg (2008)"}],"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-00593-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T18:40:19Z","timestamp":1739040019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00593-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005923","9783642005930"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00593-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}