Software verification games: Designing Xylem, The Code of Plants.

Formal software verification is a software engineering technique for modeling a software system’s source code, and then proving properties about it, such as freedom from security vulnerabilities. Though proofs are largely automated, formal source code modeling is time consuming and requires substantial human attention. Xylem: The Code of Plants is an iPad game where players make observations about unusual plants, and thereby model the behavior of software loops. With large numbers of players, the goal of Xylem is to have players model the behavior of large software systems faster, and at lower cost, than is currently achievable with formal verification experts. We present an overview of major design challenges and approaches encountered in the design of a game for crowd-sourced formal software verification. A core challenge is the need to accurately reflect the structure of real-world software source code in a game setting, without showing the source code text to players. This goal created a tension with the need to design a game that is a fun, engaging experience, which often requires simplification of the core activities of the player. Another challenge is not knowing what is the solution to a particular problem, and the resulting difficulty in providing scoring feedback to the player. These design considerations are of interest for crowd-sourcing games in general, and software engineering games in particular.