| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Translation Validation for Clock Transformations in a Synchronous Compiler
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.
Cited literature [22 references]
https://hal.inria.fr/hal-01087795
Contributor : van Chan Ngo <>
Submitted on : Friday, April 17, 2015 - 11:12:27 AM
Last modification on : Friday, January 8, 2021 - 3:40:37 AM
Long-term archiving on: : Tuesday, April 18, 2017 - 10:45:36 PM
Contributor : van Chan Ngo <>
Submitted on : Friday, April 17, 2015 - 11:12:27 AM
Last modification on : Friday, January 8, 2021 - 3:40:37 AM
Long-term archiving on: : Tuesday, April 18, 2017 - 10:45:36 PM