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 Contributor : Van Chan NgoConnect in order to contact the contributor Submitted on : Friday, April 17, 2015 - 11:12:27 AM Last modification on : Monday, June 27, 2022 - 3:02:43 AM Long-term archiving on: : Tuesday, April 18, 2017 - 10:45:36 PM
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⟩