Towards model checking of computer games with Java PathFinder

We show that Java source code of computer games can be checked for bugs such as uncaught exceptions by the model checker Java PathFinder (JPF). To model check Java games, we need to tackle the state space explosion problem and handle native calls. To address those two challenges we use our extensions of JPF, jpf-probabilistic and jpf-nhandler. The former deals with the randomization in the source code of the game, which is a cause of the state space explosion problem. The latter handles native calls automatically. We show how JPF enhanced with our extensions can check games such as the text based game Hamurabi and a graphics based version of rock-paper-scissors.