Computer Science Colloquium

Translation Validation of Optimizing Compilers

Lenore Zuck

Wednesday, April 7, 2004 11:30 A.M.
Room 1302 Warren Weaver Hall
251 Mercer Street
New York, NY 10012-1185

Colloquium Information:


Richard Cole, (212) 998-3119


There is a growing awareness, both in industry and academia, of the crucial role of formally verifying the translation from high-level source-code into low-level object code that is typically performed by an optimizing compiler. Formally verifying an optimizing compiler, as one would verify any other large program, is not feasible due to its size, ongoing evolution and modification, and, possibly, proprietary considerations. \emm{Translation validation} is a novel approach that offers an alternative to the verification of translators in general and compilers in particular: Rather than verifying the compiler itself, one constructs a validation tool which, after \emm{every} run of the compiler, formally confirms that the target code produced in the run is a correct translation of the source program. The talk will explain the concept of translation validation, and the work in the ACSys group towards achieving automatic translation validation of Intel's ORC compiler.

top | contact