Accession Number : AD1006449


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 :

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