Linked by Thom Holwerda on Thu 13th Aug 2009 15:08 UTC, submitted by Inkslinger
Thread beginning with comment 378552
To read all comments associated with this story, please click here.
To read all comments associated with this story, please click here.
It's a little baffling that the first L4 implementation certified is also the first closed source one (as far as I can see and I've been paying attention).
Do you think this may be another example of a collaborative effort shanghaied by a business once it reaches a milestone? (think darwin or webkit)
It's why I don't like open source licenses that don't require reciprocation. Such as L4's original BSD license.




Member since:
2009-06-19
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.