PROOF BY GAMES
Technical Report,01 Jun 2012,31 Oct 2015
Raytheon BBN Technologies WALTHAM United States
Pagination or Media Count:
Online gaming is popular and it would be extremely valuable if a system could harness this intellectual effort for practical purposes. In this report, we discuss two crowd-sourced, on-line games, that present players with arcade-style puzzles to solve. The puzzles in Ghost Map and Ghost Map Hyperspace are generated from a formal analysis of the correctness of a software program. In our approach, a puzzle is generated for potential flaws in the software and the crowd produces formal proofs of the softwares correctness by solving the puzzles. This report documents the challenges, lessons learned and efficiency of producing formal verification proofs of software through crowd sourced game play.