A Reasoning Engine for the Gamification of Loop-Invariant Discovery
This addresses the challenge of engaging students and software engineers in formal methods without requiring expertise, though it is incremental in applying gamification to an existing educational bottleneck.
The paper tackles the problem of making loop-invariant discovery accessible to non-experts by developing a reasoning engine that gamifies the process, enabling players to specify and verify program properties beyond automated tools within an hour.
We describe the design and implementation of a reasoning engine that facilitates the gamification of loop-invariant discovery. Our reasoning engine enables students, computational agents and regular software engineers with no formal methods expertise to collaboratively prove interesting theorems about simple programs using browser-based, online games. Within an hour, players are able to specify and verify properties of programs that are beyond the capabilities of fully-automated tools. The hour limit includes the time for setting up the system, completing a short tutorial explaining game play and reasoning about simple imperative programs. Players are never required to understand formal proofs; they only provide insights by proposing invariants. The reasoning engine is responsible for managing and evaluating the proposed invariants, as well as generating actionable feedback.