Formal verification of a realistic compiler

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.

REFERENCES

• 1: Andrew W. Appel, Foundational Proof-Carrying Code, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.247, June 16-19, 2001
• 2: 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.
• 3: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 4: 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.
• 5: Blazy, S., Leroy, X. Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning (2009). Accepted for publication, to appear.
• 6: G. J. Chaitin, Register allocation & spilling via graph coloring, Proceedings of the 1982 SIGPLAN symposium on Compiler construction, p.98-105, June 23-25, 1982, Boston, Massachusetts, United States
• 7: Coq development team. The Coq proof assistant. Available at http://coq.inria.fr/, 1989--2009.
• 8: Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
• 9: Lal George , Andrew W. Appel, Iterated register coalescing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.3, p.300-324, May 1996 [doi>10.1145/229542.229546]
• 10: Hales, T.C. Formal proof. Notices AMS 55, 11 (2008), 1370--1380.
• 11: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 12: Leroy, X. The CompCert verified compiler, software and commented proof. Available at http://compcert.inria.fr/, Aug.2008.
• 13: Leroy, X. A formally verified compiler back-end. arXiv:0902.2137 {cs}. Submitted, July 2008.
• 14: Xavier Leroy , Sandrine Blazy, Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations, Journal of Automated Reasoning, v.41 n.1, p.1-31, July 2008 [doi>10.1007/s10817-008-9099-0]
• 15: Pierre Letouzey, Extraction in Coq: An Overview, Proceedings of the 4th conference on Computability in Europe: Logic and Theory of Algorithms, p.359-369, June 15-20, 2008, Athens, Greece [doi>10.1007/978-3-540-69407-6_39]
• 16: 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.
• 17: 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.
• 18: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 19: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 20: George C. Necula, Translation validation for an optimizing compiler, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.83-94, June 18-21, 2000, Vancouver, British Columbia, Canada
• 21: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 22: Amir Pnueli , Michael Siegel , Eli Singerman, Translation Validation, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.151-166, March 28-April 04, 1998
• 23: Jean-Baptiste Tristan , Xavier Leroy, Formal verification of translation validators: a case study on instruction scheduling optimizations, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 24: Jean-Baptiste Tristan , Xavier Leroy, Verified validation of lazy code motion, Proceedings of the 2009 ACM SIGPLAN conference on Programming language design and implementation, June 15-21, 2009, Dublin, Ireland

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors