Solving Interactive Fiction Games via Partial Evaluation and Bounded Model Checking

TL;DR

This paper demonstrates how program verification tools, combined with program transformations and partial evaluation, can be used to solve simple interactive fiction games, providing insights into analyzing interpreted scripting languages.

Contribution

It introduces a novel approach of applying model-checkers and partial evaluation to solve interactive fiction games, a first in using such tools on commercial games.

Findings

Model-checkers alone cannot handle original game code.

Program transformations preserve game behavior and facilitate verification.

Partial evaluation effectively handles interpreted scripting languages.

Abstract

We present a case study on using program verification tools, specifically model-checkers for C programs, to solve simple interactive fiction games from around 1980. Off-the-shelf model-checking tools are unable to handle the games in their original form. In order to work around this, we apply a series of program transformations that do not change the behaviour of the program. An interesting aspect of these games is that they use a simple, interpreted language to script in-game events. This turns out to be the most difficult part of the program for verification tools to handle; we tackle this using partial evaluation. Our case study thus provides some insights that are applicable more generally to verification and analysis of programs that interpret scripting languages. To the best of our knowledge, this is the first example of a commercially released game being solved by application of a program model-checker to the game's code.