Verification Games: Crowd-Sourced Formal Verification

Abstract

Over the more than three years of the project Verification Games: Crowd-sourced Formal Verification the verification tools developed by the Programming Languages and Software Engineering group were improved. A series of games were developed by the Center for Game Science: Pipe Jam, Traffic Jam, Flow Jam and Paradox. Verification tools and games were integrated to verify that the Hadoop-common program satisfies constraints that render it free of the following vulnerabilities: injection attacks, incorrect use of format strings, violations of documented locking conventions.

Open PDF

Document Details

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

Entities

People

  • Michael Ernst

Organizations

  • University of Washington

Tags

DTIC Thesaurus Topics

  • Air Force
  • Air Force Research Laboratories
  • Command Injection
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Engineering
  • Government Procurement
  • Governments
  • Language
  • Operating Systems
  • Programming Languages
  • Software Development
  • User Interface
  • Verification
  • Vulnerability

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Science.
  • Game Theory.
  • Mathematical Modeling and Probability Theory.