Covac: Compiler validation by program analysis of the cross-product

Abstract. The paper presents a deductive framework for proving pro-gram equivalence and its application to automatic verification of trans-formations performed by optimizing compilers. To leverage existing pro-gram analysis techniques, we reduce the equivalence checking problem to analysis of one system- a cross-product of the two input programs. We show how the approach can be effectively used for checking equivalence of consonant (i.e., structurally similar) programs. Finally, we report on the prototype tool that applies the developed methodology to verify that a compiler optimization run preserves the program semantics. Unlike exist-ing frameworks, CoVaC accommodates absence of compiler annotations and handles most of the classical intraprocedural optimizations such as constant folding, reassociation, common subexpression elimination, code motion, dead code elimination, branch optimizations, and others.