Home » forums » LtU Forum

Verification games: Making verification fun

Verification games: Making verification fun

Abstract:
Program verification is the only way to be certain that a given piece of software is free of (certain types of) errors — errors that could otherwise disrupt operations in the field. To date, formal verification has been done by specially-trained engineers. Labor costs have heretofore made formal verification too costly to apply beyond small, critical software components.

Our goal is to make verification more cost-effective by reducing the skill set required for program verification and increasing the pool of people capable of performing program verification. Our approach is to transform the verification task (a program and a goal property) into a visual puzzle task — a game — that gets solved by people. The solution of the puzzle is then translated back into a proof of correctness. The puzzle is engaging and intuitive enough that ordinary people can through game-play become experts.

This paper presents a status report on the Verification Games project and our Pipe Jam prototype game.

By George Morrison at 2014-02-07 18:35 | LtU Forum | previous forum topic | next forum topic | other blogs | 4178 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

How practical?

I wonder at the practicality of this.

The majority of the challenge is specifying the precise properties we wish to prove in a manner amenable to constructive proof. Beyond that point, machines can play the 'game' of finding a solution. Further, if there is no solution, i.e. when the program is incorrect, there can be no proof of correctness. I think human players will not have much fun with that game!

Scoring mechanisms and 'buzzsaws' for assumptions correspond to a shift from 'satisfiability problem' to 'optimization problem'. Optimization problems often have nicer composition, strategy, and search properties than satisfiability, so it's even a good idea. But this can be done without the human.

In some ways, we should be pushing the other direction - automated testing even of 'fun' games, e.g. to ensure a solution exists with limitations on reaction speed and so on.

By dmbarbour at Fri, 2014-02-07 19:48 | login or register to post comments

Constraint satisfaction problems

Yup. It's not really a surprise that some classes of CSPs could be mapped into recreational puzzles/games while preserving some kind of intuition. But it remains to be seen whether humans actually perform better at this kind of task - particularly seeing as the authors seem to make a point of abstracting away from any domain-specific features of the original programming problem (to the point of regenerating "level names" and the like). (I see this problem class as being clearly different from, say, Foldit, where humans can rely on their intuitive spatial- and physical-processing ability.)

"Flexible CSPs" are also well-known in the relevant literature, so the same questions really apply to the relaxed problem with availability of "buzzsaws", i.e. assertions/blame points.

By vrijz at Sat, 2014-02-08 16:31 | login or register to post comments