A Denotational Translation Validator

LLVM M.D. (Mis-optimization Detector) is a compiler research project at Harvard University.

Our goal is to detect when a compiler optimization changes the meaning of the input program. This almost always indicates a bug in the optimizer.

For our project we are using the LLVM optimization framework.

Our tools work by analysing two LLVM programs and trying to determine if they have the same meaning. Our tools do not require any integration with the optimizer to work, and can also be used on hand-optimized code. This technique is called "Translation Validation", and our work is focused around scaling this technique to a real-world compiler such as LLVM.

We hope that our tools will be useful for compiler developers, and for industries where safety-critical software is important and optimization is needed.

Recent News

September 8, 2010: Updated Experimental Results
Improved and expanded experimental results have been posted using the newest version of LLVM-MD. Please see the Experimental Results section for more information.
September 7, 2010: New Version
A new version of LLVM-MD is now available. This version incorporates a alternative to structural analysis for identifying program structure, and is able to handle more functions, with a lower false alarm rate.
July 15, 2010: New Research Paper
We have posted our first research paper related to our tools: LLVM M.D.: A Denotational Translation Validator. Please see the Publications section for more information.