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

{"_id":"m63bJSEqPfkZfx6ez","bibbaseid":"leroy-formalverificationofarealisticcompiler-2009","authorIDs":[],"author_short":["Leroy, X."],"bibdata":{"bibtype":"article","type":"article","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":[{"propositions":[],"lastnames":["Leroy"],"firstnames":["Xavier"],"suffixes":[]}],"month":"July","year":"2009","note":"ZSCC: 0001022 Citation Key Alias: leroy2009","pages":"107–115","bibtex":"@article{leroy_formal_2009,\n\ttitle = {Formal {Verification} of a {Realistic} {Compiler}},\n\tvolume = {52},\n\tissn = {0001-0782},\n\turl = {http://doi.acm.org/10.1145/1538788.1538814},\n\tdoi = {10/c9sb7q},\n\tabstract = {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.},\n\tlanguage = {en},\n\tnumber = {7},\n\turldate = {2019-09-30},\n\tjournal = {Communications of the ACM},\n\tauthor = {Leroy, Xavier},\n\tmonth = jul,\n\tyear = {2009},\n\tnote = {ZSCC: 0001022\nCitation Key Alias: leroy2009},\n\tpages = {107--115}\n}\n\n","author_short":["Leroy, X."],"key":"leroy_formal_2009","id":"leroy_formal_2009","bibbaseid":"leroy-formalverificationofarealisticcompiler-2009","role":"author","urls":{"Paper":"http://doi.acm.org/10.1145/1538788.1538814"},"downloads":0},"bibtype":"article","biburl":"https://bibbase.org/zotero/k4rtik","creationDate":"2020-05-31T17:07:22.718Z","downloads":0,"keywords":[],"search_terms":["formal","verification","realistic","compiler","leroy"],"title":"Formal Verification of a Realistic Compiler","year":2009,"dataSources":["Z5Dp3qAJiMzxtvKMq"]}