@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]).},
}
