Translation validation

[Google Scholar]

Notes: CompCert compiler
Papers: pnueli:tacas:1998, necula:pldi:2000, samet:phd:1975

todo:

SeL4: Formal verification of an OS kernel [klein:sosp:2009]
Formal verification of a realistic compiler [leroy:cacm:2009]
Translation validation for an optimizing compiler [necula:pldi:2000]
Translation validation [pnueli:tacas:1998]
A machine description facility for compiler testing [samet:ieeetse:1977]
Automatically proving the correctness of translations involving optimized code. [samet:phd:1975]
Translation validation for a verified OS kernel [sewell:pldi:2013]
Scalable translation validation of unverified legacy OS code [tahat:fmcad:2019]

Notes related to Translation validation