论文标题
通过部分评估和有限模型检查解决互动小说游戏
Solving Interactive Fiction Games via Partial Evaluation and Bounded Model Checking
论文作者
论文摘要
我们提出了一项有关使用程序验证工具的案例研究，特别是用于C程序的模型检查器，以解决1980年左右的简单互动小说游戏。现成的模型检查工具无法以其原始形式处理游戏。为了解决此问题，我们应用了一系列不会改变程序行为的程序转换。这些游戏的一个有趣的方面是，他们在游戏中使用简单的，解释的语言来脚本。事实证明，这是该计划中最困难的部分来处理验证工具。我们使用部分评估来解决此问题。因此，我们的案例研究提供了一些更普遍地用于验证和分析解释脚本语言的程序的见解。 据我们所知，这是通过将程序模型检查器应用于游戏代码来解决的商业发布的游戏的第一个示例。
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.
