3 ms·

Can someone explain to me what it means for a kernel to have an end-to-end proof of implementation? Does it just mean that the kernel is implemented bug-free? T

by awhitty 12y ago

Can someone explain to me what it means for a kernel to have an end-to-end proof of implementation? Does it just mean that the kernel is implemented bug-free? That it will never panic?

klibertp 12y ago
It won't. See here: http://sel4.systems/FAQ/#verif http://sel4.systems/FAQ/#verif It's actually a very impressive piece of work, I can't wait to read about the details of how it was done.
- sanxiyn 12y ago
  Then go read http://www.nicta.com.au/pub?id=7371 http://www.nicta.com.au/pub?id=7371 :)