The Compiler Validation Project:
Developing tools for proving the correctness of compilation.

    Our goal is to develop a methodology, supported by automatic tools, which will provide practical means for ensuring provably correct compilation by state-of-the art optimizing compilers.

Our tools build on the translation validation approach, which proves the correctness of each individual compilation rather then the correctness of the entire compiler. Our preliminary results demonstrate that proving the correctness of compilations is a far more tractable problem than proving the correctness of the compiler itself.

This work benefits developers of safety-critical systems, compiler developers, and other groups of software developers for whom correctness is an important consideration.