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.

 

 

Many of the properties needed to verify a behavioral property of a program are also needed by compilers to generate high-quality, optimized machine code for a program. As compilation time is a key performance metric for compilers, and compilers are expected to be completely automated, today’s compilers generate conservative approximations of these properties, all of which are either computationally undecidable or infeasible to compute rapidly. CSFV is interested in technologies that leverage annotations developed during formal software verification to aid the compilation process, thereby generating more highly optimized code. Optimization is possible along many dimensions, e.g., performance (execution time), energy use, etc.

 

This program does not seek the development of new formal software verification tools. Modifications of existing software verification tools are within the scope of this effort.

According to last week’s notification, DARPA/I2O will conduct a briefing — CSFV Proposers’ Day — in support of the anticipated solicitation on Dec. 8, 2011, at Menlo Park, CA. The purpose of Proposers’ Day, which will be streamed live via the Web, will be:

• To familiarize participants with DARPA’s interest in innovative approaches to crowd sourced formal verification;
• To identify potential proposers and promote understanding of the anticipated CSFV … proposal requirements; [and]
• To promote discussion of synergistic capabilities among potential program participants.

Check out the Proposers’ Day website for additional details, including how to register, hotel and other local logistics, etc.

And in the meantime, visit the teaming website DARPA/I2O has created “to facilitate the formation of teaming arrangements between interested parties” — i.e., “strong, collaborative teaming efforts and business relationships” — in anticipation of the December solicitation.

(Contributed by Erwin Gianchandani, CCC Director)