Resumen:
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 verifica-
tion has been done by specially-trained engineers. Labor costs make formal verification too costly to
apply beyond small, critical software components.
Our goal is to make software verification more cost-effective by reducing the skill set required
for verification and increasing the pool of people capable of performing 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. It is publicly available to play, and game players have produced proofs of security
properties for real programs.
This talk will present the design goals and choices for both the game that the player sees and for
the underlying program analysis. It will conclude with implications to gaming, programming, and
beyond.