Translation Validation for Clock Transformations in a Synchronous CompilerReport as inadecuate




Translation Validation for Clock Transformations in a Synchronous Compiler - Download this document for free, or read online. Document in PDF available to download.

1 ESTASYS - Efficient STAtistical methods in SYstems of systems Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL 2 TEA - Tim, Events and Architectures Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL

Abstract : Translation validation was introduced as a technique to for-mally verify the correctness of code generators that attempts to verify that program transformations preserve the semantics. In this work, we adopt this approach to construct a validator that formally verifies the preservation of clock semantics during the Signal compiler transforma-tions. The clock semantics is represented as a first-order logic formula called clock model. Then we introduce a refinement relation which ex-presses 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.

Keywords : Synchronous data-flow languages Certified com-piler Formal verification Translation validation SMT solver





Author: Van Chan Ngo - Jean-Pierre Talpin - Thierry Gautier - Paul Le Guernic -

Source: https://hal.archives-ouvertes.fr/



DOWNLOAD PDF




Related documents