<p>
We present CompCertELF, the first extension to CompCert that
supports verified compilation from C programs all the way to a
standard binary file format, i.e., the ELF object format.
Previous work on Stack-Aware CompCert provides a verified
compilation chain from C programs to assembly programs with a
realistic machine memory model. We build CompCertELF by
modifying and extending this compilation chain with a verified
assembler which further transforms assembly programs into ELF
object files.
</p>

<p>
CompCert supports large-scale verification via verified separate
compilation: C modules can be written and compiled separately,
and then linked together to get a target program that refines the
semantics of the program linked from the source modules.
However, verified separate compilation in CompCert only works for
compilation to assembly programs, not to object files. For the
latter, the main difficulty is to bridge the two different views
of linking: one for CompCert's programs that allows arbitrary
shuffling of global definitions by linking and the other for
object files that treats blocks of encoded definitions as
indivisible units.
</p>

<p>
We propose a lightweight approach that solves the above problem
without any modification to CompCert's framework for verified
separate compilation: by introducing a notion of syntactical
equivalence between programs and proving the commutativity
between syntactical equivalence and the two different kinds of
linking, we are able to transit from the more abstract linking
operation in CompCert to the more concrete one for ELF object
files. By applying this approach to CompCertELF, we obtain the
first compiler that supports verified separate compilation of C
programs into ELF object files.
</p>