Slashdot is powered by your submissions, so send in your scoop


Forgot your password?
Compare cell phone plans using Wirefly's innovative plan comparison tool ×

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

"It says he made us all to be just like him. So if we're dumb, then god is dumb, and maybe even a little ugly on the side." -- Frank Zappa