Crowd-Sourced Help with Emergent Knowledge for Optimized Formal Verification (CHEKOFV)

Abstract

Formal Verification of Software is an expensive and time consuming task aimed at discovering and correcting software errors that lead to programming errors. The Crowd-Sourced Formal Verification (CSFV) program was developed to explore utilizing games to prove correctness proofs for software. Leveraging human pattern recognition skills, the CSFV games provide formal verification proofs a machine analyzing the code cannot. The SRI team developed two games; Xylem; The Code of Plants, and Binary Fission to prove Crowd Sourced game play can improve Formal Verification effectiveness and reduce the cost to verify code.

Open PDF

Document Details

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

Entities

People

  • Florent Kirchner
  • Jim Murray
  • Jim Whitehead

Organizations

  • SRI International

Tags

Communities of Interest

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

DTIC Thesaurus Topics

  • Air Force
  • Computational Science
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Debugging
  • Fission
  • Identification
  • Machine Learning
  • Network Science
  • Operating Systems
  • Pattern Recognition
  • Psychology
  • Reasoning
  • Robotics
  • Social Media

Fields of Study

  • Computer science

Readers

  • Agent-Based Social Robotics and Mobile-Assisted Learning in Virtual Environments.
  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Computer Programming and Software Development.

Technology Areas

  • AI & ML