Brian Campbell. An executable semantics for CompCert C. In Chris Hawblitzel and Dale Miller, editors, The Second International Conference on Certified Programs and Proofs (CPP 2012), volume 7679 of Lecture Notes in Computer Science, pages 60--75. Springer-Verlag, 2012. The original publication is available at www.springerlink.com. [ bib | DOI | Author's version | slides ]