Frédéric Besson, Sandrine Blazy, Pierre Wilke: A Concrete Memory Model for CompCert. ITP 2015: 67-83