Unreliable software places huge costs both on the military and the civilian economy. The current state of practice contains about one to five bugs per thousand lines of code. Formal program verification is the only way to be certain that a given piece of software is free of errors that could disrupt military operations in the field. Formal verification is currently done manually by specially-trained engineers. Consequently, formal verification has been too costly to apply beyond small, critical software components.
Unreliable software places huge costs both on the military and the civilian economy. The current state of practice contains about one to five bugs per thousand lines of code. Formal program verification is the only way to be certain that a given piece of software is free of errors that could disrupt military operations in the field. Formal verification is currently done manually by specially-trained engineers. Consequently, formal verification has been too costly to apply beyond small, critical software components.
The Crowd Sourced Formal Verification (CSFV) program seeks to make formal program verification more cost-effective by reducing the skill set required for verification. The approach is to transform verification into a more accessible task by creating a game that reflects the code model, is intuitively understandable, and is fun to play. Completion of the game effectively helps the program verification tool complete the corresponding formal program verification proof.
The primary research challenge faced by CSFV is construction of automated game-level builders capable of transforming program verification models into compelling games. A particular game instance is a function of the program verification tool, the property to be verified and the program being verified. Each game instance is provided to the “crowd”, either via the Web or through internal domain distribution. Game solutions are used to populate a database, then are mapped back into program annotations sufficient to allow the program verification tool to make progress toward verifying a specific program property.
The CSFV program was approved in the fall of 2011. A Broad Agency Announcement (BAA) is expected to be published in late 2011.