{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:51:47Z","timestamp":1725558707349},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540201014"},{"type":"electronic","value":"9783540398134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39813-4_6","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T19:27:49Z","timestamp":1277839669000},"page":"91-106","source":"Crossref","is-referenced-by-count":2,"title":["A Machine-Verified Code Generator"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Walther","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Schweitzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"http:\/\/www.informatik.tu-darmstadt.de\/pm\/verifun\/"},{"key":"6_CR2","volume-title":"Compilers: Principles, Techniques and Tools","author":"A.V. Aho","year":"1986","unstructured":"Aho, A.V., Sethi, R., Ullmann, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, New York (1986)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-45294-X_13","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"A. Dold","year":"2001","unstructured":"Dold, A., Vialard, V.: A mechanically verified compiling specification for a Lisp compiler. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 144\u2013155. Springer, Heidelberg (2001)"},{"key":"6_CR4","unstructured":"Flatau, A.D.: A Verified Implementation of an Applicative Language with Dynamic Storage Allocation. PhD. Thesis, Univ. of Texas (1992)"},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1005797629953","volume":"19","author":"J. Giesl","year":"1997","unstructured":"Giesl, J.: Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning\u00a019, 1\u201329 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR6","unstructured":"Goerigk, W., Dold, A., Gaul, T., Goos, G., Heberle, A., von Henke, H., Hoffmann, U., Langmaack, H., Zimmermann, W.: Compiler correctness and implementation verification: The Verifix approach. In: Fritzson, P. (ed.) Proc. of the Poster Session of CC 1996 - Intern. Conf. on Compiler Construction, pp. 65\u201373 (1996)"},{"key":"6_CR7","volume-title":"Semantics of Programming Languages \u2014 Structures and Techniques","author":"C.A. Gunter","year":"1992","unstructured":"Gunter, C.A.: Semantics of Programming Languages \u2014 Structures and Techniques. The MIT Press, Cambridge (1992)"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1109\/LICS.1992.185552","volume-title":"Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science","author":"J. Hannan","year":"1992","unstructured":"Hannan, J., Pfenning, F.: Compiler verification in LF. In: Scedrov, A. (ed.) Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp. 407\u2013418. IEEE Computer Society Press, Los Alamitos (1992)"},{"key":"6_CR9","volume-title":"Proc. on a Symp. in Applied Math., 19, Math. Aspects of Comp. Sc.","author":"J. McCarthy","year":"1967","unstructured":"McCarthy, J., Painter, J.A.: Correctness of a Compiler for Arithmetical Expressions. In: Schwartz, J.T. (ed.) Proc. on a Symp. in Applied Math., 19, Math. Aspects of Comp. Sc.. American Math. Society, Providence (1967)"},{"issue":"4","key":"6_CR10","first-page":"461","volume":"5","author":"J.S. Moore","year":"1989","unstructured":"Moore, J.S.: A Mechanically Verified Language Implementation. Journal of Automated Reasoning\u00a05(4), 461\u2013492 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR11","volume-title":"PITON - A Mechanically Verified Assembly-Level Language","author":"J.S. Moore","year":"1996","unstructured":"Moore, J.S.: PITON - A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"6_CR12","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-1-4757-3188-0_5","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"J.S. Moore","year":"2000","unstructured":"Moore, J.S.: An exercise in graph theory. In: Kaufmann, M., Manolios, P., Moore, J.S. (eds.) Computer-Aided Reasoning: ACL2 Case Studies, Boston, MA., pp. 41\u201374. Kluwer Academic Press, Dordrecht (2000)"},{"key":"6_CR13","volume-title":"Semantics with Applications","author":"H.R. Nielson","year":"1992","unstructured":"Nielson, H.R., Nielson, F.: Semantics with Applications. John Wiley and Sons, New York (1992)"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1109\/HOL.1991.596292","volume-title":"International Workshop on Higher Order Logic Theorem Proving and its Applications","author":"P. Curzon","year":"1991","unstructured":"Curzon, P.: A verified compiler for a structured assembly language. In: Archer, M., Joyce, J.J., Levitt, K.N., Windley, P.J. (eds.) International Workshop on Higher Order Logic Theorem Proving and its Applications, Davis, California, pp. 253\u2013262. IEEE Computer Society Press, Los Alamitos (1991)"},{"key":"6_CR15","volume-title":"Automated Deduction: A Basis for Applications","author":"G. Schellhorn","year":"1998","unstructured":"Schellhorn, G., Ahrendt, W.: The WAM case study: Verifying compiler correctness for Prolog with KIV. In: Bibel, W., Schmidt, P.H. (eds.) Automated Deduction: A Basis for Applications, vol.\u00a0III. Kluwer Academic Publishers, Dordrecht (1998)"},{"issue":"1","key":"6_CR16","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/0004-3702(94)90063-9","volume":"71","author":"C. Walther","year":"1994","unstructured":"Walther, C.: On Proving the Termination of Algorithms by Machine. Artificial Intelligence\u00a071(1), 101\u2013157 (1994)","journal-title":"Artificial Intelligence"},{"key":"6_CR17","volume-title":"Intellectics and Computational Logic","author":"C. Walther","year":"2000","unstructured":"Walther, C.: Criteria for Termination. In: H\u00f6lldobler, S. (ed.) Intellectics and Computational Logic. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Walther, C.: Semantik und Programmverifikation. Teubner-Wiley, Leipzig (2001)","DOI":"10.1007\/978-3-322-86768-1"},{"key":"6_CR19","unstructured":"Walther, C., Schweitzer, S.: A Machine Supported Proof of the Unique Prime Factorization Theorem. Technical Report VFR 02\/03, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2002)"},{"key":"6_CR20","unstructured":"Walther, C., Schweitzer, S.: The $\\surd$ eriFun Tutorial. Technical Report VFR 02\/04, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2002)"},{"key":"6_CR21","unstructured":"Walther, C., Schweitzer, S.: $\\surd$ eriFun User Guide. Technical Report VFR 02\/01, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2002)"},{"key":"6_CR22","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45085-6_1","volume-title":"Automated Deduction \u2013 CADE-19","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: About $\\surd$ eriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 1\u20135. Springer, Heidelberg (2003)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Walther, C., Schweitzer, S.: A Machine-Verified Code Generator. Technical Report VFR 03\/01, Programmiermethodik, Technische Universit\u00e4t Darmstadt (2003)","DOI":"10.1007\/978-3-540-39813-4_6"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Walther, C., Schweitzer, S.: Verification in the Classroom. To appear in Journal of Automated Reasoning - Special Issue on Automated Reasoning and Theorem Proving in Education, 1\u201321 (2003)","DOI":"10.1023\/B:JARS.0000021872.64036.41"},{"key":"6_CR25","series-title":"LNAI","first-page":"1","volume-title":"Mechanizing Mathematical Reasoning: Techniques, Tools and Applications","author":"C. Walther","year":"2003","unstructured":"Walther, C., Schweitzer, S.: A Verification of Binary Search. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning: Techniques, Tools and Applications. LNCS (LNAI), vol.\u00a02605, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"6_CR26","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. The MIT Press, Cambridge (1993)"},{"issue":"4","key":"6_CR27","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"W.D. Young","year":"1989","unstructured":"Young, W.D.: A Mechanically Verified Code Generator. Journal of Automated Reasoning\u00a05(4), 493\u2013518 (1989)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39813-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T07:33:44Z","timestamp":1591428824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39813-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540201014","9783540398134"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39813-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}