Xavier Leroy
Abstract
This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
- ]]Appel, A.W. Foundational proof-carrying code. In Logic in Computer Science 2001 (2001), IEEE, 247--258. Google Scholar
Digital Library
- ]]Appel, A.W., Blazy, S. Separation logic for small-step Cminor. In Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of LNCS (2007), Springer, 5--21. Google ScholarDigital Library
- ]]Bertot, Y., Castéran, P. Interactive Theorem Proving and Program Development---Coq'Art: The Calculus of Inductive Constructions (2004), Springer. Google ScholarDigital Library
- ]]Blazy, S., Dargaye, Z., Leroy, X. Formal verification of a C compiler front-end. In FM 2006: International Symposium on Formal Methods, volume 4085 of LNCS (2006), Springer, 460--475. Google ScholarDigital Library
- ]]Blazy, S., Leroy, X. Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning (2009). Accepted for publication, to appear.Google Scholar
- ]]Chaitin, G.J. Register allocation and spilling via graph coloring. In 1982 SIGPLAN Symposium on Compiler Construction (1982), ACM, 98--105. Google ScholarDigital Library
- ]]Coq development team. The Coq proof assistant. Available at http://coq.inria.fr/, 1989--2009.Google Scholar
- ]]Dave, M.A. Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28, 6 (2003), 2. Google ScholarDigital Library
- ]]George, L., Appel, A.W. Iterated register coalescing. ACM Trans, Prog. Lang. Syst. 18, 3 (1996), 300--324. Google ScholarDigital Library
- ]]Hales, T.C. Formal proof. Notices AMS 55, 11 (2008), 1370--1380.Google Scholar
- ]]Leroy, X. Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd Symposium on the Principles of Programming Languages (2006), ACM, 42--54. Google ScholarDigital Library
- ]]Leroy, X. The CompCert verified compiler, software and commented proof. Available at http://compcert.inria.fr/, Aug.2008.Google Scholar
- ]]Leroy, X. A formally verified compiler back-end. arXiv:0902.2137 {cs}. Submitted, July 2008.Google Scholar
- ]]Leroy, X., Blazy, S. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reasoning 41, 1 (2008), 1--31. Google ScholarDigital Library
- ]]Letouzey, P. Extraction in Coq: An overview. In Logic and Theory of Algorithms, Computability in Europe, CiE 2008, volume 5028 of LNCS (2008), Springer, 359--369. Google ScholarDigital Library
- ]]McCarthy, J., Painter, J. Correctness of a compiler for arithmetical expressions. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics (1967), AMS, 33--41.Google Scholar
- ]]Milner, R., Weyhrauch, R. Proving compiler correctness in a mechanized logic. In Proceedings of 7th Annual Machine Intelligence Workshop, volume 7 of Machine Intelligence (1972), Edinburgh University Press, 51--72.Google Scholar
- ]]Morrisett, G., Walker, D., Crary, K., Glew, N. From System F to typed assembly language. ACM Trans. Prog. Lang. Syst. 21, 3 (1999), 528--569. Google ScholarDigital Library
- ]]Necula, G.C. Proof-carrying code. In 24th Symposium on the Principles of Programming Languages (1997), ACM, 106--119. Google ScholarDigital Library
- ]]Necula, G.C. Translation validation for an optimizing compiler. In Programming Language Design and Implementation 2000 (2000), ACM, 83--95. Google ScholarDigital Library
- ]]Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W. CIL: Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction, volume 2304 of LNCS (2002), Springer, 213--228. Google ScholarDigital Library
- ]]Pnueli, A., Siegel, M., Singerman, E. Translation validation. In Tools and Algorithms for Construction and Analysis of Systems, TACAS '98, volume 1384 of LNCS (1998), Springer, 151--166. Google ScholarDigital Library
- ]]Tristan, J.-B., Leroy, X. Formal verification of translation validators: A case study on instruction scheduling optimizations. In 35th Symposium of the Principles of Programming Languages (2008), ACM, 17--27. Google ScholarDigital Library
- ]]Tristan, J.-B., Leroy, X. Verified validation of lazy code motion. In Programming Language Design and Implementation 2009 (2009), ACM. To appear. Google ScholarDigital Library
Index Terms
- Formal verification of a realistic compiler
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Compiler verification for fun and profit
FMCAD '14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided DesignFormal verification of software or hardware systems --- be it by model checking, deductive verification, abstract interpretation, type checking, or any other kind of static analysis --- is generally conducted over high-level programming or description ...
Applying Formal Verification with Protocol Compiler
DSD '01: Proceedings of the Euromicro Symposium on Digital Systems DesignAbstract: This paper presents a practical methodology for the application of formal verification to the industrial design environment "Protocol Compiler". Our verification flow is to first create a testbench and simulate the design. Then we modify the ...
Comments