{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:43:27Z","timestamp":1725515007106},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540698234"},{"type":"electronic","value":"9783540698241"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69824-1_18","type":"book-chapter","created":{"date-parts":[[2008,7,11]],"date-time":"2008-07-11T11:29:24Z","timestamp":1215775764000},"page":"316-335","source":"Crossref","is-referenced-by-count":6,"title":["Proof-Transforming Compilation of Eiffel Programs"],"prefix":"10.1007","author":[{"given":"Martin","family":"Nordio","sequence":"first","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":"18_CR1","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 (2005)","DOI":"10.1016\/j.entcs.2005.02.026"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_20","volume-title":"Static Analysis","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate Translation for Optimizing Compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134. Springer, Heidelberg (2006)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Third International Workshop on Formal Aspects in Security and Trust, Newcastle, UK, pp. 112\u2013126 (2005)","DOI":"10.1007\/11679219_9"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Chang, B., Chlipala, A., Necula, G., Schneck, R.: The Open Verifier Framework for Foundational Verifiers. In: ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2005) (2005)","DOI":"10.1145\/1040294.1040295"},{"key":"18_CR5","unstructured":"Meyer, B.: Multi-language programming: how .net does it. In: 3-part article in Software Development. May, June and July 2002, especially Part 2, http:\/\/www.ddj.com\/architect\/184414864?"},{"key":"18_CR6","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":"18_CR7","unstructured":"Meyer, B., M\u00fcller, P., Nordio, M.: A Hoare logic for a subset of Eiffel. Technical Report 559, ETH Zurich (2007)"},{"key":"18_CR8","unstructured":"Meyer, B.: ISO\/ECMA Eiffel standard (Standard ECMA-367: Eiffel: Analysis, Design and Programming Language) (June 2006), http:\/\/www.ecma-international.org\/publications\/standards\/Ecma-367.htm"},{"key":"18_CR9","unstructured":"MOBIUS Consortium. Deliverable 4.3: Intermediate report on proof-transforming compiler (2007), http:\/\/mobius.inria.fr"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Modular Specification and Verification of Object-Oriented Programs","year":"2002","unstructured":"M\u00fcller, P. (ed.): Modular Specification and Verification of Object-Oriented Programs. LNCS, vol.\u00a02262. Springer, Heidelberg (2002)"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: Sixth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS 2007), pp. 39\u201346 (2007)","DOI":"10.1145\/1292316.1292321"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Programming Language Design and Implementation (PLDI), pp. 333\u2013344. ACM Press (1998)","DOI":"10.1145\/277650.277752"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Nordio, M., M\u00fcller, P., Meyer, B.: Formalizing Proof-Transforming Compilation of Eiffel programs. Technical Report 587, ETH Zurich (2008)","DOI":"10.1007\/978-3-540-69824-1_18"},{"key":"18_CR14","unstructured":"Pavlova, M.: Java Bytecode verification and its applications. PhD thesis, University of Nice Sophia-Antipolis (2007)"},{"key":"18_CR15","unstructured":"Poetzsch-Heffter, A.: Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich (1997)"},{"key":"18_CR16","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.: A Programming Logic for Sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999 and ETAPS 1999. LNCS, vol.\u00a01576, pp. 162\u2013176. Springer, Heidelberg (1999)"},{"key":"18_CR17","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)"}],"container-title":["Lecture Notes in Business Information Processing","Objects, Components, Models and Patterns"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69824-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T16:29:36Z","timestamp":1557678576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69824-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540698234","9783540698241"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69824-1_18","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2008]]}}}