Design Lessons From Binary Fission: A Crowd Sourced Game for Precondition Discovery

Abstract

This paper introduces the formal software verification game, Binary Fission. After outlining the problem space of formal software verification games, we give a brief overview of Binary Fission. We then go into detail about several important design goals we had in mind, such as affording rapid decision making, based on other software verification games and our own past experience. We detail how Binary Fission achieves these design goals, and then talk about several design lessons we learned. We discuss lessons learned, both in the parts of the game that performed well, and in the parts that did not quite work as intended.