The Defense Advanced Research Projects Agency’s (DARPA) Information Innovation Office (I2O) announced last week its intention to issue, perhaps in December, a solicitation for Crowd Sourced Formal Verification (CSFV), with the goal of investigating “innovative approaches that automatically create games capable of transforming formal verification problems into compelling games for end users to play.”

From the official notification:

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 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. The below graphic [after the jump] depicts a notional architecture of a game solution.

 

» Read more: DARPA May Pursue Crowdsourced Software Testing