DARPA to banish “geeky, formal” way code defects are eradicated

DARPA program seeks to make complicated software code verification process into a game

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.

More news: Celebrating the birthplace of the Internet in pictures

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."

DARPA has scheduled a CSFC proposers' day workshop Dec. 8 in Menlo Park, CA .

Follow Michael Cooney on Twitter: nwwlayer8  and on Facebook

Layer 8 Extra

Check out these other hot stories:

Successful, effective IT project tips

Energy company wants to be first to mine the moon

NASA turns up ocean of water, and possibility of life, on Jupiter's moon

US Marshals selling autographed Bill Clinton saxophone, trove of other bling

DARPA wants powerful, secure wireless system to link space satellites

IBM: Analytics, mobile, cloud, social apps drive future IT development

10 petaflop Japanese supercomputer world's fastest

DARPA program looks to radically change security authentication techniques

US snapshot of broadband world finds disparity and dial-up

FBI takes out $14M DNS malware operation

DARPA gets serious with Internet security, schmoozes the dark side

"Mudge" Zatko shaking up DARPA's security software routine

US cyber chief says cloud computing can manage serious cyber threats

Join the Network World communities on Facebook and LinkedIn to comment on topics that are top of mind.

Copyright © 2011 IDG Communications, Inc.

IT Salary Survey: The results are in