Toward Gamification and Crowdsourcing of Software Verification
Software has become intimately linked with every part of our modern life, from controlling our power grids and water ways, through managing financial transactions and medical records to mediating our personal communications and social life. This increasingly complex web of programs is developed in many different languages, by different actors with varying degrees of quality control and expertise. As a result, bugs proliferate through modern software and cause failures with high human and fiscal costs.
One promising technique proposed to ensure software quality is automated software verification. In this approach, an automated tool tries to prove the software is free from entire classes of bugs. In practice however, these verification tools are not completely 'automated' -they still require a significant amount of manual effort, by a verification experts in the form of explicit annotations, carefully crafted hints or template libraries. This necessary manual labor, compounded by the scarcity of verification experts, limits the scalability of these tools to larger bodies of code.
In this dissertation we argue that we can overcome these scalability limitations, by opening up parts of the software verification process to a wider audience, through the use of Gamification and Crowdsourcing. The core insight here is that many parts of the verification problem can be encoded in games, making them more widely accessible.
We provide an empirical evaluation of this idea in the form of a numerical puzzle game encoding one of the common manual verification tasks - annotating loops with invariants. Our game requires only a high-school level understanding of algebra and a love for numerical puzzles, yet our user studies show that it enables non-experts to outperform state-of-the-art verification tools. We further discuss the design and early evaluation of a second game exposing even more aspects of the verification problem to non-experts.