Challenge Overview
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.
This project, the CSFV Community Gaming website project will provide the web site infrastructure and integration of the games. This will be a web site that is available on the Internet, and also will be delivered in a form where the server and the games can be installed and used behind a firewall.
The technologies required for this project is not finalized yet. This contest is for evaluating Drupal.