Translation Validation for Synchronous Languages

A. Pnueli, M. Siegel, and O. Shtrichman

Translation validation is an alternative 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. In order to be a practical alternative to compiler verification, a key feature of this validation is its full automation.

Since the validation process attempts to ``unravel'' the transformation 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 synchronous languages, to C. We introduce new abstraction techniques as part of the automation of our approach.

In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP 1998), volume 1443 of Lecture Notes in Computer Science, pages 235-246. Springer-Verlag, 1998.

PostScript updated, improved, and extended text. © 1998 Springer-Verlag.