SRI think tank and university turn software verification into gameplay

Software verification doesn’t sound like a fun job. It involves checking a program to ensure that it is free from common vulnerabilities. So a team of computer scientists has made a game out of it called Xylem. The iPad puzzle game helps programmers find “loop invariants,” or an important part of formal software verification.

The team at the SRI International think tank in Menlo Park, Calif., and the University of California at Santa Cruz have embraced “gamification,” or using game-like mechanics to make everyday tasks more interesting. In this case, the puzzle game will tap ordinary consumers to perform verification tasks. If they’re entertained, they can be more alert and spot more bugs. On top of that, the task of doing verification will be accessible to a wider group of people.

“The Xylem game leverages crowdsourcing techniques to search for proofs that software programs are free of vulnerabilities,” said John Murray, the program director in the computer science laboratory at SRI and principal investigator for the overall Chekofv project (short for Crowd-sourced Help with Emergent Knowledge for Optimized Formal Verification). “Pieces of software code are inserted into this engaging puzzle game, where players identify new plant species by spotting patterns in the plants’ behavior on the island. The more people that play the game and correctly identify patterns, the more pieces of code are verified that they will work with the rest of the software program – it’s like solving a gigantic jigsaw puzzle.”

The Xylem puzzle game is part of an SRI project called Chekofv. It is part of a Crowd Sourced Formal Verification program funded by the U.S. Defense Advanced Research Projects Agency (DARPA). To play the game, you don’t have to know anything about software.

The game is set in a newly discovered island called Miraflora. The player is a botanist sent to describe the many unusual flowering plants on the island. The intrepid explorer is given a “floraphase comparator” for examining the plants. Using the device, the player finds the mathematical relationships among the features of flowers on the plants. As the community of players finds and describes plants, they can then see how much of the island has been explored. The game has a storyline as well.

Xylem is one of five computer games in DARPA’s CSFV program, available on the Verigames site.

“The numbers of flowers are actually values of variables inside software loops. By finding these relationships among flowers, you’re actually describing the behavior of a loop,” explained Jim Whitehead, a professor and the chair of computer science at UCSC’s Baskin School of Engineering and the university’s principal investigator for Xylem.

Usually, finding loop invariants in software programs is a challenging task that requires training.

“It’s a hard concept to get across even to computer science students,” Whitehead said. “By turning it into a game, it becomes something that an untrained person with basic math skills can do.”

Formal software verification isn’t used much because too few people are trained to do it right.

“There aren’t enough experts to formally verify all the kinds of software that are being developed,” he said.

Patrick Lincoln, the director of the Computer Science Laboratory at SRI International, said, “The Chekofv project is an aggressive research program that addresses these complex software problems in highly innovative ways. By making formal software verification more accessible and fun, a lot more people can help increase reliability and security for critical software around the world by playing the Xylem game.”

About 20 staff, graduate students, and undergraduates at UCSC’s Center for Games and Playable Media were involved in creating the game. The game is available free in the Apple iTunes App Store and will be available for Android tablets in 2014.

UCSC and SRI are also collaborating with researchers at CEA, the French Alternative Energies and Atomic Energy Commission (Commissariat à l’énergie atomique et aux énergies alternatives) to develop tools for the formal verification process.