DARPA’s games help engineers work out coding kinks
Connecting state and local government leaders
The Defense Advanced Research Projects Agency is launching the next round of crowdsourced games that help engineers test and verify software.
With millions of lines of code being created each year, checking software for errors has become a critical, and massive, job. But demand for verification has overrun the supply of people qualified to do it. While formal program verification is the best way to scrub software of errors, it must be done manually by specialized engineers and is too expensive to use on anything other than critical software components.
“The growth of software systems over the past decade has outstripped improvements in verification,” said Michael Hsieh, a Defense Advanced Research Projects Agency program manager. “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."
To address that issue, DARPA launched a new round of games under the Crowd Sourced Formal Verification program. CSFV, which has so far proven very successful, uses online games that translate players’ actions into program annotations for common software programming languages. An initial analysis indicated that CSFV gamers generated hundreds of thousands of annotations, DARPA said.
“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 Hsieh.
Cue the gamming community
CSFV launched Verigames in 2013, which provided five free games that helped experts generate “mathematical proofs to verify the absence of important classes of flaws in software written in the ‘C’ and ‘Java’ programming languages.”
The latest wave of Verigames are designed for improved playability as well as increased software verification effectiveness:
- Dynamakr asks players to energize mysterious patterns in a cosmic puzzle machine
- Paradox asks players to use an array of tools to optimize vast networks
- Ghost Map Hyperspace asks players to battle alien invaders and seal off their hyperspace rifts
- Monster Proof asks players to explore a kingdom of monsters and solve puzzles to get rich
- Binary Fission, an atom-splitting game that asks players to mix and match quarks in the name of cybersecurity.
Other examples of government crowdsourcing to inexpensively, yet effectively take on work are the transcribing challenge by the National Archives, in which volunteers transcribe and tag historical documents to make the archived information easier for research to read and query. NASA created a desktop application that allows amateur astronomers to identify asteroids or near-Earth objects that have not been tagged by NASA’s scientists – a critically important undertaking.