UC San Diego

Human computation and crowdsourcing have been successfully proposed and applied to solve problems that are difficult to solve due to either the limitations of current computing technology or the existence of only a few experts. A common way to solve problems through human computation and crowdsourcing systems is to convert them into interactive games that target a wide audience of non-experts. Leveraging humans’ innate ability to recognize patterns, a few systems have solved the problem of synthesizing loop invariants through single-player puzzle games.

This thesis proposes to apply human computation to synthesize loop invariants by having players find them through a multiplayer game. We explain the challenges involved in designing such games and explore the advantages multiplayer games offer over single-player games in terms of players’ efficiency of solving problems and the level of fun they have.