Steven Schäfer, Sigurd Schneider, Gert Smolka: Axiomatic semantics for compiler verification. CPP 2016: 188-196