Abstract
This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the specification language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous 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
Blazy, S., Leroy, X.: Formal verification of a memory model for C-like imperative languages. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 280–299. Springer, Heidelberg (2005)
Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28(6), 2–2 (2003)
Börger, E., Fruja, N., Gervasi, V., Stärk, R.: A high-level modular definition of the semantics of C#. Theoretical Computer Science 336(2-3), 235–284 (2005)
Gurevich, Y., Huggins, J.: The semantics of the C programming language. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 274–308. Springer, Heidelberg (1993)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. Technical Report 0400001T.1, National ICT Australia, March 2004, in ACM TOPLAS (to appear) (2004)
Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler. In: Proc. Conf. on Software Engineering and Formal Methods (SEFM), Koblenz, Germany, September 2005, pp. 2–11. IEEE Computer Society Press, Los Alamitos (2005)
Leroy, X.: The Compcert certified compiler back-end – commented Coq development (2006), available online at: http://cristal.inria.fr/~xleroy
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proc. Symp. Principles Of Programming Languages (POPL), Charleston, USA, January 2006, pp. 42–54. ACM Press, New York (2006)
Nepomniaschy, V., Anureev, I., Promsky, A.: Verification-oriented language C-light and its structural operational semantics. In: Ershov Memorial Conference, pp. 103–111 (2003)
Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (December 1998)
Papaspyrou, N.: A formal semantics for the C programming language. PhD thesis, National Technical University of Athens (February 1998)
Strecker, M.: Compiler verification for C0. Technical report, Université Paul Sabatier, Toulouse (April 2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blazy, S., Dargaye, Z., Leroy, X. (2006). Formal Verification of a C Compiler Front-End. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_31
Download citation
DOI: https://doi.org/10.1007/11813040_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)