title = { Certifying assembly optimizations in {Coq} by symbolic execution with hash-consing },
    author = {Gourdin, L\'eo and Boulm\'e, Sylvain},
    year = {2021},
    pages = {2},
    team = {PACSS},
    pdf = {}, language = {en},
    abstract = {We extend the CompCert C compiler for AArch64 processors with instruction scheduling and instruction compaction. We reuse the translation validation technique of [3]: an untrusted OCaml oracle performs the translation, and a formally-verified test checks that the code produced by the oracle simulates the original code. This verified test is composed of a processor-dependent frontend (ported for AArch64) with a generic backend based on symbolic execution with hash-consing (directly reused from [3]).},


Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4002163