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.
https://hal.inria.fr/hal-01087795
Contributeur : Van Chan Ngo
<>
Soumis le : vendredi 17 avril 2015 - 11:12:27
Dernière modification le : mercredi 16 mai 2018 - 11:24:07
Document(s) archivé(s) le : mardi 18 avril 2017 - 22:45:36
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. Springer, 2015. 〈hal-01087795v3〉
