Verification games: Making verification fun

Download: PDF, slides (PDF), slides (ODP), project homepage, video, Pipe Jam game, Traffic Jam game, Flow Jam game, Paradox game.

“Verification games: Making verification fun” by Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Nathaniel Mote, Brian Walker, Seth Cooper, Timothy Pavlik, and Zoran Popović. In FTfJP 2012: 14th Workshop on Formal Techniques for Java-like Programs, (Beijing, China), June 12, 2012, pp. 42-49.

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.

Download: PDF, slides (PDF), slides (ODP), project homepage, video, Pipe Jam game, Traffic Jam game, Flow Jam game, Paradox game.

BibTeX entry:

@inproceedings{DietlDEMWCPP2012,
   author = {Werner Dietl and Stephanie Dietzel and Michael D. Ernst and
	Nathaniel Mote and Brian Walker and Seth Cooper and Timothy Pavlik
	and Zoran Popovi{\'c}},
   title = {Verification games: Making verification fun},
   booktitle = {FTfJP 2012: 14th Workshop on Formal Techniques for
	Java-like Programs},
   pages = {42--49},
   address = {Beijing, China},
   month = {June~12,},
   year = {2012}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.