Formal Verification of a Realistic Compiler

被引：736

作者：

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 [J].

Appel, AW .

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 [J].

George, L ;

Appel, AW .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1996, 18 (03) :300-324

[10]

Hales T. C., 2008, NOT AM MATH SOC, V55, P1370

← 1 2 3 →