Amir Pnueli, Michael Siegel and Eli Singerman, "Translation Validation",
proceedings of TACAS'98, LNCS 1384, pp 151--166, 1998.
Abstract
We present the notion of translation validation
as a new approach to the verification 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 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.
Several ingredients are necessary to set up the -- fully
automatic -- translation validation process, among which are:
- A common semantic framework for the representation of the
source code and the generated target code.
- A formalization of the notion of "correct implementation" as a
refinement relation.
- 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-flow language Signal to asynchronous (sequential)
C-code.
Postscript (456K).