A Formally Verified Compiler Back-end. Leroy, X. Journal of Automated Reasoning, 43(4):363, November, 2009. ZSCC: 0000493
A Formally Verified Compiler Back-end [link]Paper  doi  abstract   bibtex   
This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: 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_formally_2009,
	title = {A {Formally} {Verified} {Compiler} {Back}-end},
	volume = {43},
	issn = {1573-0670},
	url = {https://doi.org/10.1007/s10817-009-9155-4},
	doi = {10/cnrcnn},
	abstract = {This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its soundness. Such a verified compiler is useful in the context of formal methods applied to the certification of critical software: 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 = {4},
	urldate = {2019-10-24},
	journal = {Journal of Automated Reasoning},
	author = {Leroy, Xavier},
	month = nov,
	year = {2009},
	note = {ZSCC: 0000493},
	keywords = {Compiler transformations and optimizations, Compiler verification, Formal methods, Program proof, Semantic preservation, The Coq theorem prover},
	pages = {363}
}

Downloads: 0