Translation Validation for Clock Transformations in a Synchronous Compiler - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Translation Validation for Clock Transformations in a Synchronous Compiler

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (385.78 Ko) Télécharger le fichier
main (1).pdf (385.78 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01087795 , version 1 (26-11-2014)
hal-01087795 , version 2 (21-12-2014)
hal-01087795 , version 3 (17-04-2015)

Identifiants

  • HAL Id : hal-01087795 , version 3

Citer

van Chan Ngo, Jean-Pierre Talpin, Thierry Gautier, Paul Le Guernic. Translation Validation for Clock Transformations in a Synchronous Compiler. FASE - ETAPS 2015, Apr 2015, London, United Kingdom. ⟨hal-01087795v3⟩
322 Consultations
245 Téléchargements

Partager

Gmail Facebook X LinkedIn More