{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:47:43Z","timestamp":1743101263773,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642025709"},{"type":"electronic","value":"9783642025716"}],"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-02571-6_12","type":"book-chapter","created":{"date-parts":[[2009,6,26]],"date-time":"2009-06-26T10:15:30Z","timestamp":1246011330000},"page":"195-214","source":"Crossref","is-referenced-by-count":11,"title":["A Sound and Complete Program Logic for Eiffel"],"prefix":"10.1007","author":[{"given":"Martin","family":"Nordio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristiano","family":"Calcagno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Naumann, J.D.A., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 387\u2013411. Springer, Heidelberg (2008)"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Bannwart, F.Y., M\u00fcller, P.: A Logic for Bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE). ENTCS, vol.\u00a0141(1), pp. 255\u2013273. Elsevier, Amsterdam (2005)","DOI":"10.1016\/j.entcs.2005.02.026"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: Towards Practical Verification for Java. In: OOPSLA 2008: Proceedings of the 23rd ACM SIGPLAN conference on Object oriented programming systems languages and applications, pp. 213\u2013226 (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, pp. 284\u2013303. Springer, Heidelberg (2000)"},{"key":"12_CR5","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":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/11526841_4","volume-title":"FM 2005: Formal Methods","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., M\u00fcller, P.: Modular Verification of Static Class Invariants. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 26\u201342. Springer, Heidelberg (2005)"},{"key":"12_CR7","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"12_CR8","unstructured":"Meyer, B. (ed.): ISO\/ECMA Eiffel standard (Standard ECMA-367: Eiffel: Analysis, Design and Programming Language) (June 2006), \n                    \n                      http:\/\/www.ecma-international.org\/publications\/standards\/Ecma-367.htm"},{"key":"12_CR9","unstructured":"MOBIUS Consortium. Deliverable 3.1: Byte code level specification language and program logic (2006), \n                    \n                      http:\/\/mobius.inria.fr"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems, pp. 39\u201346 (2007)","DOI":"10.1145\/1292316.1292321"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Nordio, M., Calcagno, C., M\u00fcller, P., Meyer, B.: Soundness and Completeness of a Program Logic for Eiffel. Technical Report 617, ETH Zurich (2009)","DOI":"10.1007\/978-3-642-02571-6_12"},{"key":"12_CR12","series-title":"LNBIP","volume-title":"TOOLS-EUROPE 2008","author":"M. Nordio","year":"2008","unstructured":"Nordio, M., M\u00fcller, P., Meyer, B.: Proof-Transforming Compilation of Eiffel Programs. In: Paige, R., Meyer, B. (eds.) TOOLS-EUROPE 2008. LNBIP, vol.\u00a011. Springer, Heidelberg (2008)"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL\u00a02004, pp. 268\u2013280 (2004)","DOI":"10.1145\/982962.964024"},{"key":"12_CR14","first-page":"247","volume-title":"POPL 2005","author":"M.J. Parkinson","year":"2005","unstructured":"Parkinson, M.J., Bierman, G.: Separation logic and abstraction. In: POPL 2005, vol.\u00a040, pp. 247\u2013258. ACM Press, New York (2005)"},{"key":"12_CR15","first-page":"75","volume-title":"POPL\u00a02008","author":"M.J. Parkinson","year":"2008","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL\u00a02008, pp. 75\u201386. ACM Press, New York (2008)"},{"key":"12_CR16","unstructured":"Pavlova, M.: Java Bytecode verification and its applications. PhD thesis, University of Nice Sophia-Antipolis (2007)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: Logical Foundations for Typed Object-Oriented Languages. In: Gries, D., De Roever, W. (eds.) Programming Concepts and Methods (PROCOMET), pp. 404\u2013423 (1998)","DOI":"10.1007\/978-0-387-35358-6_26"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-49099-X_11","volume-title":"Programming Languages and Systems","author":"A. Poetzsch-Heffter","year":"1999","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.O.: A Programming Logic for Sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"key":"12_CR19","unstructured":"Poetzsch-Heffter, A., Rauch, N.: Soundness and Relative Completeness of a Programming Logic for a Sequential Java Subset. Technical report, Technische Universit\u00e4t Kaiserlautern (2004)"},{"key":"12_CR20","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"12_CR21","unstructured":"Schoeller, B.: Making classes provable through contracts, models and frames. PhD thesis, ETH Zurich (2007)"},{"key":"12_CR22","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. In: Formal Techniques for Java-like Programs (2008)"},{"key":"12_CR23","unstructured":"von Oheimb, D.: Analyzing Java in Isabelle\/HOL - Formalization, Type Safety and Hoare Logic. PhD thesis, Universit\u00e4t M\u00fcnchen (2001)"}],"container-title":["Lecture Notes in Business Information Processing","Objects, Components, Models and Patterns"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02571-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T18:50:40Z","timestamp":1558378240000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02571-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642025709","9783642025716"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02571-6_12","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2009]]}}}