PROOF BY GAMES

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 2016
Accession Number
AD1006449

Entities

People

  • Kerry Moffitt
  • Michelle Spina

Organizations

  • BBN Technologies

Tags

Communities of Interest

  • Autonomy
  • Biomedical
  • Cyber
  • Energy and Power Technologies
  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Air Force
  • C Programming Language
  • Cognitive Systems Engineering
  • Computer Program Documentation
  • Computer Program Reliability
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Cybersecurity
  • Debugging
  • Electronic Mail
  • Lessons Learned
  • Operating Systems
  • Software Development
  • Video Games
  • Web Browsers

Fields of Study

  • Computer science

Readers

  • Distributed Systems and Data Platform Development
  • Game Theory.
  • Software Engineering.