4 ms·
The formal C semantics are defined in Isabelle/HOL, checked, and then the compiler output is also checked. They use standard GCC compilers for all of this. See
by mondoshawan 5y ago
The formal C semantics are defined in Isabelle/HOL, checked, and then the compiler output is also checked. They use standard GCC compilers for all of this.
See https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-binary-code/ https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-bi...