Verification games: Making software verification fun

Michael Ernst, U Washington

Software engineering:
   mathematics (modeling, analysis), but there is an non-ideal component: people!

Crowd-sourced software verification.

Programming is like a game. But when is it not fun?

Code ---> automatically translated--->Game---->People palying--->Completed game ----> Automatic translated -----> Verified software (with proof/annotations)

Idea:
Encodes a constraint system for both code and game.


Example:
Code:Assiginment can only go from a type to its supertype.(variable: ball, assignment variable: pipe)
Code: null pointer errors (small ball: non null value, big ball: null vablue, pipe: dereference)
Game: ball can only fall into pipes wider than the ball
Cheats: cut the ball size to win unwinnable game (bug detected!)
Most accurate ituition: type constraints
Different pipes of the same color at different board: different use of the same variable
Different boards: different methods of a class
Level: a class
You need to solve all boards of one level at once. (Non-local reasoning)

Type flow vs. data flow:
Good for type flow (no loops, specif values, etc), not good for data flow

Other examples:
SQL injection
race conditions and deadlocks (if you use lock)
unintended side effetects

Why type systems for verification is good for games:
Modular, local reasoning and non-understanding

3-way collaboration: machines, players, verification experts
Machine optimization: simplify the challenge to its essence. (Abstract interpretation, constraint propagation, heuristic sovling) --- to make the game high level, playable. Too much details: player distracted, too little detail: unable to produce useful result.
Players: utilizing a community (20000 yrs people spent playing angry birds until 2011!), game design point. Same problem can have different skins --- different game.

Game requirment: abstraction (easy playng), modularity( different people work on different parts of the program)

Scoring System: Guide people to do more effective verification. In some sense, designing a good scoring system is the whole problem.


Why not covert everything into SAT and gamefy SAT:
Size explords and destroys problem structure thus no human intuition

Big questions:
How do we gamify software engineering, or even computer tasks in general?