@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}
}

{"_id":"viNSSwvAQeydhJ84E","bibbaseid":"leroy-aformallyverifiedcompilerbackend-2009","authorIDs":[],"author_short":["Leroy, X."],"bibdata":{"bibtype":"article","type":"article","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":[{"propositions":[],"lastnames":["Leroy"],"firstnames":["Xavier"],"suffixes":[]}],"month":"November","year":"2009","note":"ZSCC: 0000493","keywords":"Compiler transformations and optimizations, Compiler verification, Formal methods, Program proof, Semantic preservation, The Coq theorem prover","pages":"363","bibtex":"@article{leroy_formally_2009,\n\ttitle = {A {Formally} {Verified} {Compiler} {Back}-end},\n\tvolume = {43},\n\tissn = {1573-0670},\n\turl = {https://doi.org/10.1007/s10817-009-9155-4},\n\tdoi = {10/cnrcnn},\n\tabstract = {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.},\n\tlanguage = {en},\n\tnumber = {4},\n\turldate = {2019-10-24},\n\tjournal = {Journal of Automated Reasoning},\n\tauthor = {Leroy, Xavier},\n\tmonth = nov,\n\tyear = {2009},\n\tnote = {ZSCC: 0000493},\n\tkeywords = {Compiler transformations and optimizations, Compiler verification, Formal methods, Program proof, Semantic preservation, The Coq theorem prover},\n\tpages = {363}\n}\n\n","author_short":["Leroy, X."],"key":"leroy_formally_2009","id":"leroy_formally_2009","bibbaseid":"leroy-aformallyverifiedcompilerbackend-2009","role":"author","urls":{"Paper":"https://doi.org/10.1007/s10817-009-9155-4"},"keyword":["Compiler transformations and optimizations","Compiler verification","Formal methods","Program proof","Semantic preservation","The Coq theorem prover"],"downloads":0},"bibtype":"article","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.680Z","downloads":0,"keywords":["compiler transformations and optimizations","compiler verification","formal methods","program proof","semantic preservation","the coq theorem prover"],"search_terms":["formally","verified","compiler","back","end","leroy"],"title":"A Formally Verified Compiler Back-end","year":2009,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}