Re: [seL4] Joint a formally verified C compiler with seL4?

Hello,

I think SeL4 research team has already discussed this point and proposed binary verification alternative. Please check 4.7 in

http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml

Cheers,

Julien

On 03/02/2015 10:49 AM, Grissiom wrote:

Hi all,

I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 .

So what benefit will there be if some one use CompCert as the compiler for seL4?

-- Cheers, Grissiom

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel