{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:07:50Z","timestamp":1725505670365},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787389"},{"type":"electronic","value":"9783540787396"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78739-6_24","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:39:06Z","timestamp":1207125546000},"page":"307-321","source":"Crossref","is-referenced-by-count":18,"title":["Verification of Equivalent-Results Methods"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"24_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":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"24_CR3","first-page":"100","volume-title":"Computer Security Foundations (CSFW)","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations (CSFW), pp. 100\u2013114. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"24_CR4","first-page":"23","volume":"7","author":"R.M. Burstall","year":"1972","unstructured":"Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. Machine Intelligence\u00a07, 23\u201350 (1972)","journal-title":"Machine Intelligence"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamari\u0107, Z.: A Reachability Predicate for Analyzing Low-Level Software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"key":"24_CR6","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/582419.582447","volume-title":"OOPSLA","author":"D.G. Clarke","year":"2002","unstructured":"Clarke, D.G., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA. SIGPLAN Notices, vol.\u00a037(11), pp. 292\u2013310. ACM Press, New York (2002)"},{"key":"24_CR7","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. SIGPLAN Notices, vol.\u00a033(10), pp. 48\u201364. ACM Press, New York (1998)"},{"issue":"8","key":"24_CR8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.5381\/jot.2005.4.8.a4","volume":"4","author":"D. Cok","year":"2005","unstructured":"Cok, D.: Reasoning with specifications containing method calls and model fields. Journal of Object Technology\u00a04(8), 77\u2013103 (2005)","journal-title":"Journal of Object Technology"},{"key":"24_CR9","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)"},{"issue":"5","key":"24_CR10","doi-asserted-by":"crossref","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)","journal-title":"Journal of Object Technology"},{"key":"24_CR11","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (March 2005)"},{"key":"24_CR12","unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. PhD thesis, Katholieke Universiteit Leuven (2007)","DOI":"10.1007\/11901433_23"},{"key":"24_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"I.T. Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","first-page":"108","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"J.R. Kiniry","year":"2005","unstructured":"Kiniry, J.R., Cok, D.R.: ESC\/Java2: Uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 108\u2013128. Springer, Heidelberg (2005)"},{"key":"24_CR16","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":"G.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. Kluwer Academic Publishers, Dordrecht (1999)"},{"issue":"1\u20133","key":"24_CR17","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"G.T. Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Science of Computer Programming\u00a055(1\u20133), 185\u2013208 (2005)","journal-title":"Science of Computer Programming"},{"key":"24_CR18","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., M\u00fcller, P., Kiniry, J.: JML reference manual. Dept. Comp. Sci., Iowa State University (2007), http:\/\/www.jmlspecs.org"},{"key":"24_CR19","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":"24_CR20","volume-title":"2006 Marktoberdorf Summer School on Programming Methodology","author":"K.R.M. Leino","year":"2007","unstructured":"Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. In: 2006 Marktoberdorf Summer School on Programming Methodology, Springer, Heidelberg (to appear, 2007), research.microsoft.com\/~leino\/papers.html"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11863908_18","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D.A. Naumann","year":"2006","unstructured":"Naumann, D.A.: From Coupling Relations to Mated Invariants for Checking Information Flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 279\u2013296. Springer, Heidelberg (2006)"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL, pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"key":"24_CR23","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1145\/1040305.1040326","volume-title":"POPL","author":"M.J. Parkinson","year":"2005","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: POPL, pp. 247\u2013258. ACM Press, New York (2005)"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: Logical foundations for typed object-oriented languages. In: Programming Concepts and Methods (PROCOMET), pp. 404\u2013423 (1998)","DOI":"10.1007\/978-0-387-35358-6_26"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-540-30579-8_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Salcianu","year":"2005","unstructured":"Salcianu, A., Rinard, M.: Purity and Side Effect Analysis for Java Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 199\u2013215. Springer, Heidelberg (2005)"},{"issue":"1","key":"24_CR26","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1145\/792548.611987","volume":"35","author":"D.E. Stevenson","year":"2003","unstructured":"Stevenson, D.E., Phillips, A.T.: Implementing object equivalence in Java using the template method design pattern. SIGCSE Bulletin\u00a035(1), 278\u2013282 (2003)","journal-title":"SIGCSE Bulletin"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78739-6_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T11:35:23Z","timestamp":1684323323000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78739-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787389","9783540787396"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78739-6_24","relation":{},"subject":[]}}