seL4 kernel is formally verified
John van V.
john.van.v at gmail.com
Mon Aug 17 04:34:27 CEST 2009
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.
On Sun, Aug 16, 2009 at 9:26 PM, Gernot Heiser<gernot at cse.unsw.edu.au> wrote:
> 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
> l4-hackers mailing list
> l4-hackers at os.inf.tu-dresden.de
More information about the l4-hackers