Communications of the ACM
Code Breakthrough Delivers Safer Computing
"The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake," says UNSW Professor and NICTA researcher Gernot Heiser.
Credit: The University of New South Wales
Computer researchers at the University of New South Wales and NICTA say they have proven that an operating-system kernel was 100 percent free of bugs. The team verified the kernel known as the seL4 microkernel by mathematically proving the correctness of about 7,500 lines of computer code in a project taking an average of six people more than five years.
"What we've shown is that it's possible to make the lowest level, the most critical, and in a way the most dangerous part of the system, provably fault free," says NICTA researcher Gernot Heiser. The research could potentially improve the security and reliability of critical systems used by the medical and airline industries as well as the military.
"The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake," Heiser says.
From University of New South Wales
View Full Article
Abstracts Copyright © 2009 Information Inc., Bethesda, Maryland, USA 
No entries found