Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] low-level code formalisations in Isabelle


view this post on Zulip 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: Sep 25 2021 at 08:21 UTC