Prof. Mike Ernst
University of Washington
ACL2 Seminar, Dec. 2, 2013

Verification games:  Making software verification fun

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.  It is publicly available to play.

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.