Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!


Forgot your password?
DEAL: For $25 - Add A Second Phone Number To Your Smartphone for life! Use promo code SLASHDOT25. Also, Slashdot's Facebook page has a chat bot now. Message it for stories and more. Check out the new SourceForge HTML5 Internet speed test! ×

Comment Re:World's First Formally-Proven OS Kernel - NOT (Score 1) 517

Back At-cha

Virgil's paper talks about the HARDWARE verification (also important, but...) not the software verification.

The SCOMP OS was general purpose. It had a Unix emulation layer over its kernel similar to BSD over Mach. And the kernel WAS verified. The Unix System-call layer was modelled and verified against a security model. They have 10000 theorems, we had about 3500. They use Isabell, we used Boyer-Moore. Sounds like a fairly similar approach.

And you are right: It was a very cool piece of work for the time. I am not trying to denigrate the referenced paper. It sounds wonderful and I look forward to reading it. I just object to terms like "unique" and "first".

Slashdot Top Deals

"The Avis WIZARD decides if you get to drive a car. Your head won't touch the pillow of a Sheraton unless their computer says it's okay." -- Arthur Miller