Lambda the Ultimate

Anna Zaks and Amir Pnueli (2008). CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In Proc. 15th Symp. Formal Methods.

From the introduction:

In this paper, we present a Compiler Verification by Program Analysis of the Cross-Product framework (CoVaC ) - a novel translation validation approach, in which one constructs a comparison system - a cross-product of the source and target programs. The input programs are equivalent if and only if the comparison system satisfies a certain specification. This allows us to leverage the existing methods of proving properties of a single program instead of relying on program analysis and proof rules specialized to translation validation, used by the existing frameworks.

and

Finally, this paper reports on a prototype tool CoVaC that applies the developed framework to verification of optimizing transformations performed by LLVM 1.9 - a very aggressive open-source compiler.