acm-header
Sign In

Communications of the ACM

ACM TechNews

Code Breakthrough Delivers Safer Computing


View as: Print Mobile App Share:
University of New South Wales Professor Gernot Heiser

"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

Sign In for Full Access
» Forgot Password? » Create an ACM Web Account