Formal Verification of a Realistic Compiler. Leroy, X. Communications of the ACM, 52(7):107–115, July, 2009. ZSCC: 0001022 Citation Key Alias: leroy2009
Formal Verification of a Realistic Compiler [link]Paper  doi  abstract   bibtex   
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.
@article{leroy_formal_2009,
	title = {Formal {Verification} of a {Realistic} {Compiler}},
	volume = {52},
	issn = {0001-0782},
	url = {http://doi.acm.org/10.1145/1538788.1538814},
	doi = {10/c9sb7q},
	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.},
	language = {en},
	number = {7},
	urldate = {2019-09-30},
	journal = {Communications of the ACM},
	author = {Leroy, Xavier},
	month = jul,
	year = {2009},
	note = {ZSCC: 0001022
Citation Key Alias: leroy2009},
	pages = {107--115}
}

Downloads: 0