Programming C, C++, Java, PHP, Ruby, Turing, VB
Computer Science Canada 
Programming C, C++, Java, PHP, Ruby, Turing, VB  

Username:   Password: 
 RegisterRegister   
 Read about this on news.ycombinator.com
Index -> General Discussion
View previous topic Printable versionDownload TopicSubscribe to this topicPrivate MessagesRefresh page View next topic
Author Message
btiffin




PostPosted: Tue Jun 24, 2014 4:39 pm   Post subject: Read about this on news.ycombinator.com

seL4, supposedly a proven bug-free microkernel. About to go open.

http://sel4.systems/About/

(The home page had 34 days left on the countdown to release timer when I looked)

Quote:

Completely unique about seL4 is its unprecedented degree of assurance, achieved through formal verification.
Specifically, the ARM version of seL4 is the first (and still only) general-purpose OS kernel with a full functional
correctness proof, meaning a mathematical proof that the implementation (written in C) adheres to its specification.
In short, the implementation is proved to be bug-free. This implies a number of other properties, such as freedom
from buffer overflows, null pointer exceptions, use-after-free, etc.


I'm old now, but I find this hard to believe, also lazy enough to have not read the formal theory or proof papers.

Cheers
Sponsor
Sponsor
Sponsor
sponsor
Display posts from previous:   
   Index -> General Discussion
View previous topic Tell A FriendPrintable versionDownload TopicSubscribe to this topicPrivate MessagesRefresh page View next topic

Page 1 of 1  [ 1 Posts ]
Jump to:   


Style:  
Search: