The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
CompCert — a formally verified optimizing compiler
The work
| Authors | X. Leroy; S. Blazy; D. Kästner; B. Schommer; M. Pister; C. Ferdinand |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2016 |
| Citekey | leroy2016compcert |
Where it appeared
| Published in | Embedded Real Time Software and Systems |
|---|
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-10-26 04:52 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@inproceedings{leroy2016compcert,
title = {CompCert — a formally verified optimizing compiler},
author = {X. Leroy and S. Blazy and D. Kästner and B. Schommer and M. Pister and C. Ferdinand},
year = {2016},
booktitle = {Embedded Real Time Software and Systems},
}
This record lives at https://refs.drheap.org/leroy2016compcert/ and will keep doing so.