Translation Validation

Abstract

(joint work with Amir Pnueli and Michael Siegel)

In this talk, we first (briefly) describe the general trend of applying formal methods to safety critical systems. Then, we concentrate on a key issue in this framework: verifying the compilation from a synchronous design language (e.g., SIGNAL) to an implementable asynchronous code (e.g., C).

We present our new fully automatic method of Translation Validation. The idea of translation validation is the following: 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., 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 code.

We demonstrate the intuition behind our approach by an example and finally, outline the formal method.