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


Forgot your password?
Check out the new SourceForge HTML5 internet speed test! No Flash necessary and runs on all devices. ×

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

"Pascal is Pascal is Pascal is dog meat." -- M. Devine and P. Larson, Computer Science 340