bibtex

@inproceedings{GB1,
    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 = {https://coq-workshop.gitlab.io/2021/abstracts/Coq2021-04-01-certifying-optimizations-hash-consing.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]).},
}

URL


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

info visites 4086853