Formal Verification of a Realistic Compiler

被引：701
作者：
Leroy, Xavier [1 ]
机构：
[1] INRIA, Paris, France
来源：
COMMUNICATIONS OF THE ACM | 2009年 / 52卷 / 07期
关键词：
D O I：
10.1145/1538788.1538814
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：107 / 115
页数：9
相关论文
共 24 条
  • [1] [Anonymous], 1989, COQ PROOF ASSISTANT
  • [2] [Anonymous], 2003, ACM SIGSOFT Softw. Eng. Notes, DOI DOI 10.1145/966221.966235
  • [3] Appel AW, 2007, LECT NOTES COMPUT SC, V4732, P5
  • [4] Foundational proof-carrying code
    Appel, AW
    [J]. 16TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2001, : 247 - 256
  • [5] Bertot Y., 2004, TEXT THEORET COMP S
  • [6] BLAZY S, 2009, J AUTOM RES IN PRESS
  • [7] Blazy S, 2006, LECT NOTES COMPUT SC, V4085, P460
  • [8] CHAITIN GJ, 1982, 1982 SIGPLAN S COMP, P98
  • [9] Iterated register coalescing
    George, L
    Appel, AW
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1996, 18 (03): : 300 - 324
  • [10] Hales T. C., 2008, NOT AM MATH SOC, V55, P1370
123