The initial phase of a DARPA program that used publicly accessible online games to accelerate the verification of software has helped produce hundreds of thousands of program annotations in common software programming languages, adding credence to the idea that digital games can be an effective means of crowdsourcing solutions to software problems. The results have inspired DARPA to launch a new round of games with the goal of extending the successes to date and learning more about the approach's potential.
"We're excited by these results and are encouraging the public to play our new games over the next few weeks so we can see just how far this approach may go," said Michael Hsieh, DARPA program manager. "The growth of software systems over the past decade has outstripped improvements in verification. There are simply not enough experts to provide manual analysis on the scale required to support formal verification of the countless software systems launched every day."
Unreliable software imposes significant costs on the U.S and global economies. Existing development practices result in software that contains about one to five bugs or errors per thousand lines of code. Formal program verification--mathematical approach to ensuring the fundamental accuracy of code--is the best way to be certain that a given piece of software is free of certain types of errors. But formal verification today is almost always done manually by specially-trained engineers, and is too costly to apply beyond small, critical software components.
In December 2013, DARPA's Crowd Sourced Formal Verification (CSFV) program launched the first version of the Verigames web portal (www.verigames.com), which offered five free online formal verification games. These games translated players' actions into program annotations and assisted formal verification experts in generating mathematical proofs to verify the absence of important classes of flaws in software written in the "C" and "Java" programming languages. An initial analysis indicates that non-experts playing CSFV games generated hundreds of thousands of annotations.
To learn more about the potential of this approach to crowdsourcing verification, CSFV recently released five new games on www.verigames.com, designed for improved playability as well as increased software verification effectiveness:
CSFV games are open only to players ages 18 and up.
You are now leaving the DARPA.mil website that is under the control and
management of DARPA. The appearance of hyperlinks does not constitute
endorsement by DARPA of non-U.S. Government sites or the information,
products, or services contained therein. Although DARPA may or may not
use these sites as additional distribution channels for Department of
Defense information, it does not exercise editorial control over all of
the information that you may find at these locations. Such links are
provided consistent with the stated purpose of this website.
After reading this message, click to continue