Follow Slashdot blog updates by subscribing to our blog RSS feed


Forgot your password?
Slashdot Deals: Deal of the Day - Pay What You Want for the Learn to Code Bundle, includes AngularJS, Python, HTML5, Ruby, and more. ×

Submission + - World's first fully formally proven OS ( 2

An anonymous reader writes: Operating systems usually have bugs — the `blue screen of death', the amiga Hand, etc., are known by almost everyone. NICTA's team of researchers has managed to produce an OS kernel that can NEVER crash, and is guaranteed to meet its specification. It is fully formally verified — as such it exceeds the Common Criteria's highest level of assurance.

The researchers used an executable specification written in Haskell, C code that mapped to the Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system.

"For the love of phlegm...a stupid wall of death rays. How tacky can ya get?" - Post Brothers comics