CompCert

CompCert is a C compiler. It is developed and formally verified in the Coq proof assistant.

The CompCert project is headed by Xavier Leroy.

History

The CompCert project originally targeted a fairly large subset of C - called Clight - which it compiled to PowerPC assembly code Leroy 2009.

It has since been extended to cover almost all of ISO C 2011, generating code for ARM, PowerPC, RISC-V, and x86.

For the development of CompCert, seven researchers received the 2021 ACM Software System Award.

References

• Official website

• Wikipedia page

• YouTube video for the 2021 ACM Software System Award.

• A 2009 report on the CompCert project is given in the CACM article

@article{10.1145/1538788.1538814,
	author = {Leroy, Xavier},
	title = {Formal Verification of a Realistic Compiler},
	year = {2009},
	issue_date = {July 2009},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	volume = {52},
	number = {7},
	issn = {0001-0782},
	url = {https://doi.org/10.1145/1538788.1538814},
	doi = {10.1145/1538788.1538814},
	journal = {Commununications of the ACM},
	month = {jul},
	pages = {107–115},
	numpages = {9}
}