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

Download
Author
Yilmaz, Mehmet
Date
2015-09Advisor
Xie, Geoffrey G.
Second Reader
Cook, Glenn R.
Metadata
Show full item recordAbstract
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.
Rights
Copyright is reserved by the copyright owner.Collections
Related items
Showing items related by title, author, creator and subject.
-
Formal models of a least privilege separation kernel in alloy
Phelps, David; Levin, Timothy E.; Auguston, Mikhail (International Conference on i-Warfare and Security, 2008-06-01);We describe the specification of the formal security policy model and formal top-level specification for the Least Privilege Separation Kernel (LPSK) in Alloy, a relatively new modelling language and analysis tool. The ... -
An analysis of Specware and its usefulness in the verification of high assurance systems
DeCloss, Daniel P. (Monterey, California. Naval Postgraduate School, 2006-06);Formal verification is required for systems that require high assurance. Formal verification can require large and complex proofs that can drastically affect the development life cycle. Through the use of a verification ... -
Crowdsourced formal verification: a business case analysis toward a human-centered business model
Baur, Andreas (Monterey, California: Naval Postgraduate School, 2015-06);The DARPA project Crowd Sourced Formal Verification (CSFV) tries to investigate whether offering free games via the Internet that translate player’s actions into program annotations helps to overcome the challenges of the ...