2 ms·
Dr. Dobbs: Proving The Correctness of an OS Kernel (using Haskell and Isabelle)
- grandinj 17y agoExecutive summary: Took them 5 years to formally verify 7500 lines of kernel code. Good luck doing that with a real kernel - linux is more than 2.4 million lines of code