The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi Gregory.

Some years ago, Jean-François Monin, Xiaomu Shi, myself and a few other people developed some tools to semi automatically compile to C and Coq code the ARM documentation. We used it for ARMv6 and SHv4. The generated C code has been integrated in the system on chip simulator SimSoC and used on real examples. It's not maintained anymore but you will perhaps find it useful. See https://gforge.inria.fr/projects/simsoc-cert/ .

Best regards,

Frédéric.

Le 01/06/2018 à 19:12, Gregory Malecha a écrit :

Hello --

I am wondering if anyone knows of a formalization of the ARMv8 (or other instruction set) in Coq that is open source. I'm looking for as complete of an instruction set as possible since I am working with low-level systems programs.

Thanks so much.

--

- gregory malecha
  gmalecha.github.io