L4 microkernels: The lessons from 20 years of research and deployment

Re:L4 microkernels: The lessons from 20 years of research an... by pjmlp on Tuesday September 20, 2016 @12:09PM (#12540601)

Not really, to verify C code you need to set the compiler and its corresponding version in stone for the verification process, as UB can change even between versions of the same compiler.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @12:11PM (#12540630)

Not really true. See https://www.nicta.com.au/publications/research-publications/... for how the compiler and its internal semantics are completely removed from the chain for l4v.

[ Parent | on HN ]

Re:L4 microkernels: The lessons from 20 years of research an... by pjmlp on Wednesday September 21, 2016 @02:57AM (#12545977)

Thanks for the link, I will have a look into it.

[ Parent | on HN ]