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