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):

Report Date:

2016-03-01

Pagination or Media Count:

120.0

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.

Subject Categories:

Distribution Statement:

APPROVED FOR PUBLIC RELEASE