TVOC: A Translation Validator for Optimizing Compilers:

Click here for Source Code

TVOC Manual

Sample Programs:

We present two programs verified by TVOC. Both source and target are Intermediate Representations(IR) translated by SGI Pro64 from C program. Source is the IR without optimization, and Target is the IR after a series of optimizations.

Example 1

Source    Target    VCs


Example 2

Source    Target    VCs