Translation Validation for Clock Transformations in a Synchronous CompilerReportar como inadecuado




Translation Validation for Clock Transformations in a Synchronous Compiler - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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





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

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



DESCARGAR PDF




Documentos relacionados