Please create an account to participate in the Slashdot moderation system


Forgot your password?
Slashdot Deals: Cyber Monday Sale Extended! Courses ranging from coding to project management - all eLearning deals 20% off with coupon code "CYBERMONDAY20". ×

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".

"Of course power tools and alcohol don't mix. Everyone knows power tools aren't soluble in alcohol..." -- Crazy Nigel