Frédéric Besson, Sandrine Blazy, Pierre Wilke: CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. ITP 2017: 81-97