Werner Dietl
Verification Games: Making Verification Fun
VCLA will be hosting a RiSE seminar talk by Werner Dietl on June 20th, 2012.
DATE: | Wednesday, June 20, 2012 |
TIME: | 11:00 – 12:00 |
VENUE: | Library E185.1, Argentinierstrasse 8, 4th floor |
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 manually, 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 talk presents the status of the Verification Games project and our Pipe Jam prototype game.
The accompanying tutorial Developing and using pluggable type systems will take place at the same day from 14:00 to 16:00 at the same venue.