Framework for Evaluating Loop Invariant Detection Games in Relation to Automated Dynamic Invariant Detectors

Abstract

Software has a huge and negative impact on the economy. Formal verification is an effective method to check whether a piece of software contains certain kinds of errors. Defense Advanced Research Projects Agency (DARPA) started the Crowd Sourced Formal Verification (CSFV) program to propose a new model for formal verification by using five online games. CSFV aims to explore whether an online game player with no formal verification expertise can achieve formal verification more efficiently than through conventional processes. We observe that, currently, no quality criteria exist to measure CSFV gamers efforts. The study suggests that machine detectability of a solution detected by a gamer indicates poor quality for that solution. The solutions in one of the games, StormBound, were selected for examination. An automated tool was developed to check the machine detectability of the solutions, and 78 percent of the assertions were seen to be machine detectable.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2015
Accession Number
AD1009345

Entities

People

  • Mehmet Yilmaz

Organizations

  • Naval Postgraduate School

Tags

Communities of Interest

  • C4I
  • Cyber

DTIC Thesaurus Topics

  • Basic Programming Language
  • C Programming Language
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Control Systems
  • Cybersecurity
  • Detection
  • Detectors
  • Information Science
  • Operating Systems
  • Programming Languages
  • Robotics
  • Software Development
  • Software Testing
  • Spreadsheet Software

Fields of Study

  • Computer science

Readers

  • Game Theory.
  • Software Engineering.
  • Systems Analysis and Design