Validation of Interprocedural Optimizations

Amir Pnueli and Anna Zaks

New York University, NY, USA

Translation validation is an approach of ensuring compilation correctness in which each compiler run is followed by a validation pass that proves that the target code produced by the compiler is a correct translation of the source code. We present a framework for translation validation of compiler optimization run that targets reactive procedural programs. Our algorithm is automatic and accommodates most classical interprocedural optimizations such as global constant propagation, inlining, tail-recursion elimination, interprocedural dead code elimination, dead argument elimination, and cloning.

Keywords: compiler, verification, translation validation, interprocedural optimizations, program equivalence, deductive verification, formal methods.