Translation Validation is an alternative for verifying translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verification), each individual translation (i.e. a run of the compiler) is followed by a validation phase which verifies that the target code produced on this run correctly implements the submitted source program. In order to be a practical alternative to compiler verification, a key feature of this validation is full automation.
Since the validation process attempts to "unravel" the transformations
effected by the translators, its task becomes increasingly more
difficult (and necessary) with the increase of sophistication and
variety of the optimizations methods employed by the translator. In
this paper we demonstrate the practicability of translation validation
for highly optimizing, industrial code generators from DC+, a widely
used intermediate format for synchronuous languages, to C. We
introduce new abstraction techniques as part of the automation of our
approach.
International Colloquium on Automata, Languages and Programming