Translation Validation for Transformations on Abstract Clocks in Synchronous Languages

Translation validation was introduced as a technique to formally verify the correctness of code generators that attempts to verify that program transformations preserve the semantics. In this work, we adopt this approach to formally verify that the clock semantics is preserved during the transformations of a synchronous data-flow compiler. We represent the clock semantics of a program and its transformed counterpart as first-order formulas which are called clock models. Then we introduce a refinement relation which expresses the preservation of clock semantics, as a relation on clock models. Our validator does not require any instrumentation or modification of the compiler, nor any rewriting of the source program.