Joint a formally verified C compiler with seL4?
2 Mar
2015
2 Mar
'15
8:49 p.m.
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
4041
Age (days ago)
4041
Last active (days ago)
2 comments
3 participants
participants (3)
-
Gernot Heiser -
Grissiom -
Julien Iguchi-Cartigny