DARPA to banish “geeky, formal” Way Code Defects are Eradicated

By | November 25, 2011

Source: Network World

By Layer 8

For every 1,000 lines of code, one to five bugs are introduced. And getting those bugs out of the millions of lines of software code that run today’s complex systems is costly and only performed by highly specialized researchers with deep knowledge of software and mathematical theorem-proving techniques.

Those are a few of the main issues researchers at DARPA are up against and the ones they want to change dramatically with a new program announced today called Crowd Sourced Formal Verification (CSFV) that seeks to use the general public as much as possible to take on the intricate and difficult task of getting the defects out of software code.

The idea is to “game-ify” geeky formal software verification techniques by applying game-like, crowdsourced solutions to the formal verification problem, said Drew Dean, DARPA’s program manager for CSFV.  The program exploits a large user base requiring no formal verification expertise, he said.

From DARPA’s program announcement: “Currently, formal program verification is not widely practiced due to high costs and the fact that fundamental program verification problems resist automation. This is particularly an issue for the Department of Defense because formal verification, while a proven method for reducing defects in software, currently requires highly specialized talent and cannot be scaled to the size of software found in modern weapon systems.

The goal of the CSFV Program is to make formal verification of software more cost-effective by enabling non-specialists to participate productively in the formal verification process. The approach is to transform the formal verification of the property and software being verified into a game that is intuitively understandable by ordinary people and fun to play. A particular game would be a function of the formal verification tool and of the property and software being verified. Each solution of the game would enable the formal verification tool to help complete the corresponding formal software verification proof.

CSFV will investigate innovative approaches that automatically create games capable of transforming formal software verification problems into compelling games for end users to play. CSFV research picks up at a point where the formal verification tool needs human assistance. Game solutions will populate a database and be mapped back into program annotations sufficient to allow the formal verification tool to make progress towards verifying a specific property.”

“CSFV seeks to expand the Nation¹s formal verification capabilities and determine whether these enhanced capabilities are also relevant to highly optimizing compilers,” Dean said. “This program takes a radically different approach to producing correct software and offers interesting new challenges to both the formal methods and game development communities.”

Leave a Reply