{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214179},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672623"},{"type":"electronic","value":"9783540464259"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46425-5_19","type":"book-chapter","created":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T02:00:14Z","timestamp":1185933614000},"page":"290-304","source":"Crossref","is-referenced-by-count":2,"title":["On the Translation of Procedures to Finite Machines"],"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":[[2000,5,12]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"E. B\u00f6rger and I. Durdanovi\u0107. Correctness of compiling Occam to transputer code. The Computer Journal, 39(1), 1996.","DOI":"10.1093\/comjnl\/39.1.52"},{"issue":"2","key":"19_CR2","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 TOPLAS, 8(2):185\u2013214, April 1986.","journal-title":"ACM TOPLAS"},{"key":"19_CR3","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":"19_CR4","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":"8","key":"19_CR5","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"C. A. R. Hoare","year":"1987","unstructured":"C. A. R. Hoare, I. J. Hayes, H. Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorenson, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672\u2013687, August 1987.","journal-title":"Communications of the ACM"},{"key":"19_CR6","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":"19_CR7","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":"19_CR8","unstructured":"J. S. Moore. Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, 1996."},{"key":"19_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verfication: A Refinement-Algebraic Approach Advocating Stepwise Abstraction","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"M. M\u00fcller-Olm. Modular Compiler Verfication: A Refinement-Algebraic Approach Advocating Stepwise Abstraction, LNCS 1283. Springer-Verlag, 1997."},{"key":"19_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1107","DOI":"10.1007\/3-540-48118-4_9","volume-title":"FM\u2019 99","author":"M. M\u00fcller-Olm","year":"1999","unstructured":"M. M\u00fcller-Olm and A. Wolf. On excusable and inexcusable failures: towards an adequate notion of translation correctness. In FM\u2019 99, LNCS 1709, pp. 1107\u20131127. Springer-Verlag, 1999."},{"key":"19_CR11","unstructured":"H. R. Nielson and F. Nielson. Semantics with Applications: A Formal Introduction. Wiley, 1992."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"T. S. Norvell. Machine code programs are predicates too. In 6th Refinement Workshop, Workshops in Computing. Springer-Verlag and British Computer Society, 1994.","DOI":"10.1007\/978-1-4471-3240-0_10"},{"key":"19_CR13","unstructured":"E. Pofahl. Methods used for inspecting safety relevant software. In High Integrity Programmable Electronics, pages 13\u201314. Dagstuhl-Sem.-Rep. 107, 1995."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46425-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T16:28:50Z","timestamp":1556728130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46425-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672623","9783540464259"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-46425-5_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}