Abstract. We present the notion of translation validation as a new approach to the veri cation of translators (compilers, code generators). Rather than proving in advance that the compiler always produces a target code which correctly implements the source code (compiler verication), each individual translation (i.e. a run of the compiler) is followed by a validation phase which veri es that the target code produced on this run correctly implements the submitted source program. Several ingredients are necessary to set up the { fully automatic { translation validation process, among which are: 1. A common semantic framework for the representation of the source code and the generated target code. 2. A formalization of the notion of "correct implementation" as a renement relation. 3. A syntactic simulation-based proof method which allows to automatically verify that one model of the semantic framework, representing the produced target code, correctly implements another model which represents the source. These, and other ingredients are elaborated in this paper, in which we illustrate the new approach in a most challenging case. We consider a translation (compilation) from the synchronous multi-clock data-ow language Signal to asynchronous (sequential) C-code.
Verifying that the translation performed by the Seam compiler is correct is a translation validation problem REF ] that is not addressed here.
Translation Validation
TACAS
Computer Science