Framework for evaluating loop invariant detection games in relation to automated dynamic invariant detectors

Simple item page
dc.contributor.advisorXie, Geoffrey G.
dc.contributor.authorYilmaz, Mehmet
dc.contributor.departmentInformation Sciences (IS)
dc.contributor.secondreaderCook, Glenn R.
dc.dateSep-15
dc.date.accessioned2015-11-06T18:22:58Z
dc.date.available2015-11-06T18:22:58Z
dc.date.issued2015-09
dc.description.abstractSoftware 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.en_US
dc.description.distributionstatementApproved for public release; distribution is unlimited.
dc.description.serviceCaptain, Turkish Armyen_US
dc.description.urihttp://archive.org/details/frameworkforeval1094547350
dc.identifier.urihttps://hdl.handle.net/10945/47350
dc.publisherMonterey, California: Naval Postgraduate Schoolen_US
dc.rightsCopyright is reserved by the copyright owner.en_US
dc.subject.authorCrowdsourcingen_US
dc.subject.authorsoftware securityen_US
dc.subject.authorfuzzingen_US
dc.subject.authorformal verificationen_US
dc.subject.authorautomated loop invariant detectionen_US
dc.subject.authorloop invariant analysisen_US
dc.subject.authorparseren_US
dc.subject.authorHaskell languageen_US
dc.titleFramework for evaluating loop invariant detection games in relation to automated dynamic invariant detectorsen_US
dc.typeThesisen_US
dspace.entity.typePublication
etd.thesisdegree.disciplineInformation Technology Managementen_US
etd.thesisdegree.grantorNaval Postgraduate Schoolen_US
etd.thesisdegree.levelMastersen_US
etd.thesisdegree.nameMaster of Science in Information Technology Managementen_US
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
15Sep_Yilmaz_Mehmet.pdf
Size:
1.18 MB
Format:
Adobe Portable Document Format
Download
Collections
Theses