{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:56Z","timestamp":1761611216386},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665885"},{"type":"electronic","value":"9783540481188"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48118-4_9","type":"book-chapter","created":{"date-parts":[[2007,11,14]],"date-time":"2007-11-14T01:30:57Z","timestamp":1195003857000},"page":"1107-1127","source":"Crossref","is-referenced-by-count":3,"title":["On excusable and inexcusable failures towards an adequate notion of translation correctness"],"prefix":"10.1007","author":[{"given":"Markus","family":"M\u00fcller-Olm","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Wolf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"9_CR1","unstructured":"A. V. Aho, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"K.-R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Springer-Verlag, 2nd edition, 1997.","DOI":"10.1007\/978-1-4757-2714-2"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"E. B\u00fcrger and I. Durdanovi\u0107. Correctness of compiling Occam to transputer code. The Computer Journal, 39(1), 1996.","DOI":"10.1093\/comjnl\/39.1.52"},{"key":"9_CR5","first-page":"128","volume":"50","author":"J. P. Bowen","year":"1993","unstructured":"J. P. Bowen et al. A ProCoS II project description: ESPRIT Basic Research project 7071. Bulletin of the EATCS, 50:128\u2013137, June 1993.","journal-title":"Bulletin of the EATCS"},{"issue":"2","key":"9_CR6","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/5397.30847","volume":"8","author":"L. M. Chirica","year":"1986","unstructured":"L. M. Chirica and D. F. Martin. Towards compiler implementation correctness proofs. ACM Transactions on Programming Languages and Systems, 8(2):185\u2013214, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR7","unstructured":"J. W. de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall, 1980."},{"key":"9_CR8","unstructured":"E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976."},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-3228-5"},{"key":"9_CR10","series-title":"IDA Technical Report LiTH-IDA-R-96-12","first-page":"65","volume-title":"Proc. Poster Session CC\u201996","author":"W. Goerigk","year":"1996","unstructured":"W. Goerigk, A. Dold, T. Gaul, G. Goos, A. Heberle, F. Henke, U. Hoffmann, H. Langmaack, H. Pfeifer, H. Ruess, and W. Zimmermann. Compiler correctness and implementation verification: The Verifix approach. In P. Fritzson, editor, Proc. Poster Session CC\u201996, pages 65\u201373, IDA Technical Report LiTH-IDA-R-96-12, Link\u2205ping, Sweden, 1996."},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"D. Gries. The Science of Programming. Springer-Verlag, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF01128406","volume":"8","author":"J. D. Guttman","year":"1995","unstructured":"J. D. Guttman, J. D. Ramsdell, and M. Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8:5\u201332, 1995.","journal-title":"Lisp and Symbolic Computation"},{"issue":"10","key":"9_CR13","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576\u2013583, 1969.","journal-title":"Communications of the ACM"},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C. A. R. Hoare","year":"1993","unstructured":"C. A. R. Hoare, H. Jifeng, and A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30:701\u2013739, 1993.","journal-title":"Acta Informatica"},{"issue":"3","key":"9_CR15","first-page":"41","volume":"39","author":"H. Langmaack","year":"1997","unstructured":"H. Langmaack. Software engineering for certification of systems: Specification, implementation, and compiler correctness (in German). Informationstechnik und Technische Informatik, 39(3):41\u201347, 1997.","journal-title":"Informationstechnik und Technische Informatik"},{"key":"9_CR16","unstructured":"J. S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"C. Morgan and T. Vickers, editors. On the Refinement Calculus. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-3273-8"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"J. M. Morris","year":"1987","unstructured":"J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9:287\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"P. D. Mosses. Action Semantics. Cambridge University Press, 1992.","DOI":"10.1017\/CBO9780511569869"},{"key":"9_CR20","volume-title":"Advanced compiler design implementation","author":"S. S. Muchnick","year":"1997","unstructured":"S. S. Muchnick. Advanced compiler design implementation. Morgan Kaufmann Publishers, San Francisco, California, 1997."},{"key":"9_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"M. M\u00fcller-Olm. Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283. Springer-Verlag, 1997."},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"T. S. Norvell. Machine code programs are predicates too. In D. Till, editor, 6th Refinement Workshop, Workshops in Computing. Springer-Verlag and British Computer Society, 1994.","DOI":"10.1007\/978-1-4471-3240-0_10"},{"key":"9_CR23","unstructured":"E. Pofahl. Methods used for inspecting safety relevant software. In W. J. Cullyer, W. A. Halang, and B. J. Kr\u00e4mer, editors, High Integrity Programmable Electronics, pages 13\u201314. Dagstuhl-Sem.-Rep. 107, 1995."},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"S. Sippu and E. Soisalon-Soininen. Parsing Theory Vol. I. Springer-Verlag, 1988.","DOI":"10.1007\/978-3-642-61345-6"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"W. M. Waite and G. Goos. Compiler Construction. Springer-Verlag, 1984.","DOI":"10.1007\/978-1-4612-5192-7"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"R. Wilhelm and D. Maurer. \u00dcbersetzerbau. Springer, 1992.","DOI":"10.1007\/978-3-662-00077-9"}],"container-title":["Lecture Notes in Computer Science","FM\u201999 \u2014 Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48118-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T11:29:45Z","timestamp":1556969385000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48118-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665885","9783540481188"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-48118-4_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}