Inferring Loop Invariants through Gamification

論文URL:http://dl.acm.org/citation.cfm?doid=3173574.3173805

論文アブストラクト:In today's modern world, bugs in software systems incur significant costs. One promising approach to improve software quality is automated software verification. In this approach, an automated tool tries to prove the software correct once and for all. Although significant progress has been made in this direction, there are still many cases where automated tools fail. We focus specifically on one aspect of software verification that has been notoriously hard to automate: inferring loop invariants that are strong enough to enable verification. In this paper, we propose a solution to this problem through gamification and crowdsourcing. In particular, we present a puzzle game where players find loop invariants without being aware of it, and without requiring any expertise on software verification. We show through an experiment with Mechanical Turk users that players enjoy the game, and are able to solve verification tasks that automated state-of-the-art tools cannot.

日本語のまとめ:

現代では,ソフトウェアシステムのバグには大きなコストがかかる.自動ソフトウェア検証では失敗する難しいソフトウェア検証もある.このソフトウェアを使うことで,専門家じゃないプレイヤーによっていくつかの難しい問題が解決した.

(111文字)

発表スライド: