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 > [email protected] > https://sel4.systems/lists/listinfo/devel > _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
