Framework for evaluating loop invariant detection games in relation to automated dynamic invariant detectors
Loading...
Authors
Yilmaz, Mehmet
Subjects
Crowdsourcing
software security
fuzzing
formal verification
automated loop invariant detection
loop invariant analysis
parser
Haskell language
software security
fuzzing
formal verification
automated loop invariant detection
loop invariant analysis
parser
Haskell language
Advisors
Xie, Geoffrey G.
Date of Issue
2015-09
Date
Sep-15
Publisher
Monterey, California: Naval Postgraduate School
Language
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.
Type
Thesis
Description
Series/Report No
Department
Information Sciences (IS)
Organization
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
Copyright is reserved by the copyright owner.