Abstract.
We consider the machine-supported verification of a code generator computing machine code from WHILE-programs, i.e. abstract syntax trees which may be obtained by a parser from programs of an imperative programming language. We motivate the representation of states developed for the verification, which is crucial for success, as the interpretation of tree-structured WHILE-programs differs significantly in its operation from the interpretation of the linear machine code. This work has been developed for a course to demonstrate to the students the support gained by computer-aided verification in a central subject of computer science, boiled down to the classroom-level. We report about the insights obtained into the properties of machine code as well as the challenges and efforts encountered when verifying the correctness of the code generator. We also illustrate the performance of the \(\checkmark\) eriFun system that was used for this work.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aho, A.V., Sethi, R., Ullmann, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, New York (1986)
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. 2245, pp. 144–155. Springer, Heidelberg (2001)
Flatau, A.D.: A Verified Implementation of an Applicative Language with Dynamic Storage Allocation. PhD. Thesis, Univ. of Texas (1992)
Giesl, J.: Termination of Nested and Mutually Recursive Algorithms. Journal of Automated Reasoning 19, 1–29 (1997)
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–73 (1996)
Gunter, C.A.: Semantics of Programming Languages — Structures and Techniques. The MIT Press, Cambridge (1992)
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–418. IEEE Computer Society Press, Los Alamitos (1992)
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)
Moore, J.S.: A Mechanically Verified Language Implementation. Journal of Automated Reasoning 5(4), 461–492 (1989)
Moore, J.S.: PITON - A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, Dordrecht (1996)
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–74. Kluwer Academic Press, Dordrecht (2000)
Nielson, H.R., Nielson, F.: Semantics with Applications. John Wiley and Sons, New York (1992)
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–262. IEEE Computer Society Press, Los Alamitos (1991)
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. III. Kluwer Academic Publishers, Dordrecht (1998)
Walther, C.: On Proving the Termination of Algorithms by Machine. Artificial Intelligence 71(1), 101–157 (1994)
Walther, C.: Criteria for Termination. In: Hölldobler, S. (ed.) Intellectics and Computational Logic. Kluwer Academic Publishers, Dordrecht (2000)
Walther, C.: Semantik und Programmverifikation. Teubner-Wiley, Leipzig (2001)
Walther, C., Schweitzer, S.: A Machine Supported Proof of the Unique Prime Factorization Theorem. Technical Report VFR 02/03, Programmiermethodik, Technische Universität Darmstadt (2002)
Walther, C., Schweitzer, S.: The \(\surd\)eriFun Tutorial. Technical Report VFR 02/04, Programmiermethodik, Technische Universität Darmstadt (2002)
Walther, C., Schweitzer, S.: \(\surd\)eriFun User Guide. Technical Report VFR 02/01, Programmiermethodik, Technische Universität Darmstadt (2002)
Walther, C., Schweitzer, S.: About \(\surd\)eriFun. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 1–5. Springer, Heidelberg (2003)
Walther, C., Schweitzer, S.: A Machine-Verified Code Generator. Technical Report VFR 03/01, Programmiermethodik, Technische Universität Darmstadt (2003)
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–21 (2003)
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. 2605, pp. 1–18. Springer, Heidelberg (2003)
Winskel, G.: The Formal Semantics of Programming Languages. The MIT Press, Cambridge (1993)
Young, W.D.: A Mechanically Verified Code Generator. Journal of Automated Reasoning 5(4), 493–518 (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Walther, C., Schweitzer, S. (2003). A Machine-Verified Code Generator. In: Vardi, M.Y., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2003. Lecture Notes in Computer Science(), vol 2850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39813-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-39813-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20101-4
Online ISBN: 978-3-540-39813-4
eBook Packages: Springer Book Archive