Mawhorter, R. (CSE) – Certified Synthesis for Interactive Media: High Assurance Metroidvania Generation

Program verification has been applied in many contexts (including videogames), but 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. My research 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. In pursuit of this goal, I develop novel abstraction strategies that can be reapplied in other contexts. I also 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. My 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.

Event Host: Ross Mawhorter, PhD Candidate, Computer Science & Engineering

Advsior: Adam Smith