Verification Games: Making 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. The authors' 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. Their 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.