TVOC: A translation validator for optimizing compilers

Abstract

We describe a tool called TVOC, that uses the translation validation approach to check the validity of compiler optimizations: for a given source program, TVOC proves the equivalence of the source code and the target code produced by running the compiler. There are two phases to the verification process: the first phase verifies loop transformations using the proof rule PERMUTE; the second phase verifies structure-preserving optimizations using the proof rule VALIDATE. Verification conditions are validated using the automatic theorem prover CVC Lite. © Springer-Verlag Berlin Heidelberg 2005.