@inproceedings{appel_vst_2011,
 title = {Verified {Software} {Toolchain}},
 author = {Appel, Andrew W.},
 year = {2011},
 booktitle = {Programming {Languages} and {Systems} ({ESOP} 2011)},
 series = {Lecture {Notes} in {Computer} {Science}},
 publisher = {Springer},
 note = {Separation logic for Clight, sound against CompCert's semantics; the logic is a client of the compiler, not a component of it.}
}