seL4 kernel is formally verified

[John van V.]

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 Heiser<gernot at 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 at os.inf.tu-dresden.de
> http://os.inf.tu-dresden.de/mailman/listinfo/l4-hackers
>



-- 
Empathy
http://thinman.com/empathy

Photography
http://thinman.com/photography

Technology
http://thinman.com