Email Gateway (Jan 04 2021 at 08:46): Email Gateway (Jan 04 2021 at 08:46):From: Buday Gergely via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
what architectures can I target for a verifying compiler using Isabelle?
What I see is Isabelle specifications for WebAssembly:
https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf
and ARM, RISC-V and CHERI-MIPS:
https://www.cl.cam.ac.uk/~nk480/sail-submitted.pdf
Is there anything else? And, what are the limitations of the above? Any
experience report is welcome.
Last updated: Jul 15 2022 at 23:21 UTC