It would be really nice to create some plain-langauge text for the general public so that it knows the significance of this L4 milestone.
John
On Sun, Aug 16, 2009 at 9:26 PM, Gernot Heisergernot@cse.unsw.edu.au wrote:
Hi,
For those out there who missed the publicity (incl ./): NICTA announced last week that the formal verification of our seL4 kernel has been completed. This makes seL4 the first ever general-purpose OS kernel with a formal proof that the implementation is consistent with the specification.
A paper on the project will appear in this year's SOSP.
Details at http://ertos.nicta.com.au/news/home.pml#verified
Gernot
l4-hackers mailing list l4-hackers@os.inf.tu-dresden.de http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers