LLVM M.D.: A Denotational Translation Validator. This research paper presents the key ideas of the algorithm implemented in LLVM M.D.

Evaluating Value-Graph Translation Validation for LLVM. By Jean-Baptiste Tristan, Paul Govereau and Greg Morrisett. In ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation (PLDI'11).

Denotational Translation Validation. A Dissertation presented by By Paul Govereau.