Accession Number : AD1006449


Title :   PROOF BY GAMES


Descriptive Note : Technical Report,01 Jun 2012,31 Oct 2015


Corporate Author : Raytheon BBN Technologies WALTHAM United States


Personal Author(s) : Spina,Michelle ; Moffitt,Kerry


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/1006449.pdf


Report Date : 01 Mar 2016


Pagination or Media Count : 120


Abstract : 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.


Descriptors :   computer program verification , software , software development , game theory , computer programming


Distribution Statement : APPROVED FOR PUBLIC RELEASE