A Reasoning Engine for the Gamification of Loop-Invariant Discovery

TL;DR

This paper presents a browser-based reasoning engine that gamifies loop-invariant discovery, enabling users without formal methods expertise to collaboratively prove properties of simple programs within an hour.

Contribution

It introduces a novel online platform that simplifies loop-invariant discovery through gamification, making formal reasoning accessible to non-experts.

Findings

Players can specify and verify program properties within an hour.

The system supports collaborative reasoning without requiring formal proof knowledge.

Players provide invariants that the engine evaluates and uses to guide the proof process.

Abstract

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.