Linked by Thom Holwerda on Thu 13th Aug 2009 15:08 UTC, submitted by Inkslinger
OSNews, Generic OSes Australian research organisation NICTA claims to be the world's first to develop a formal machine-checked proof of a general-purpose operating system kernel, the Secure Embedded L4 (seL4). The organisation "beat" several other larger and better funded organisations to claim this achievement, according to a spokesperson.
Permalink for comment 378552
To read all comments associated with this story, please click here.
by waid0004 on Fri 14th Aug 2009 22:59 UTC
Member since:

This is really quite an awesome achievement. The ability to formally verify so much code is needed with software's increasing real world applications. My only hesitation is that the code doesn't seem to be available under an open license.

Reply Score: 1