Translation validation was introduced as a technique to formally verify the correctness of code generators that attempts to ensure that program transformations preserve the semantics of input program. In this work, we adopt this approach to construct a validator that formally verifies the preservation of clock semantics during the
compiler transformations. The clock semantics is represented as a first-order logic formula called
. We then introduce a
which expresses 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.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten