Chekofv: Crowd-sourced Formal Verification

ABSTRACT. Over the past year, we have been developing Chekofv, a system for crowd-sourced formal verification. Chekofv starts with an at- tempt to verify a given C program using the source code analysis plat- form Frama-C. Every time the analysis loses precision while analyzing looping control-flow, Chekofv tries to obtain an invariant to regain precision using crowd-sourcing. To that end, Chekofv translates the problem of finding loop invariants into a puzzle game and presents it to players of a game, Xylem, that is being developed as part of the Chekofv system. In this paper, we report on the design and implementation of the Chekofv system, the challenges and merits of gamification of the invariants detection problem, and problems and obstacles that we have encountered so far.