Content area
This dissertation uses videogames as a practical application of Formal Methods. Program verification has been applied in many contexts (including video games), but
A) The scale and complexity of the examples that have been analyzed fall short of the ability to analyze many existing games without massive computational costs.
B) Most of these analyses fail to account for the capabilities of the human player who is actually playing the game.
This dissertation focuses on automatic analysis and design of one particular game: Super Metroid, with the goal of creating general methods for efficient analysis that address these issues.
Because metroidvania games have properties that make them hard to formally analyze, studying them requires the development of new abstraction techniques in order to make this analysis feasible. In this dissertation, I develop novel abstraction strategies that can be reapplied in other contexts.
In addition to analyzing games, I show that these same techniques can also be used to synthesize games, and I develop a paradigm for understanding procedural generation problems as verification problems. This paradigm enables generators to certify their output, and these certificates act as a powerful debugging tool, giving developers specific advice on how to refine their code in order to provably improve playability. This iterative process allows for the creation of high assurance generators, whose outputs are almost always correct. By solving synthesis problems as verification problems, my methods enable large-scale, precise, and efficient analysis of entire generative spaces.
This research expands on existing techniques for applying symbolic search to large state spaces, exploring many different ways of optimizing the state space representation, and reporting on their relative effectiveness in real-world contexts. I also demonstrate how multiple layers of abstraction can be used to enhance existing search algorithms. Using these methods, I show how verifying properties of software with respect to the humans that interact with it can be practically achieved.
