Publications

Formal Verification of Interactive Visual Novels. Analysing the Structure of Interactive Stories to Find Out What Makes Them Fun

Elisabeth Lempa. Master’s Thesis in Computer Science, University of Munich, 2024.

Abstract What makes visual novels fun? In this work, we create metrics to operationalise the contribution of visual novel story structure to video game enjoyment in five different categories. We present a formal verification tool for the Ren'Py language, Ren'Py being one of the most popular visual novel engines. This formal verification tool allows to specify certain properties about a Ren'Py program, and verify whether they hold on every possible path through the game. We give formal specifications of the metrics we created. Finally, we evaluate the metrics' ability to distinguish visual novels with regards to the categories the metrics each were based on, and present additional applications of the tools we developed.

co[co]²nut. Concurrently Virtualising User Code Compilation

Elisabeth Lempa. Bachelor’s Thesis in Computer Science, University of Munich, 2018.

Abstract This thesis describes the conception and development of a concurrent virtualisation software for the e-learning platform Backstage 2. This concurrent code compile unit coconut2 ties a REST-API to dynamic creation of Docker containers in order to compile and execute user code in a secure, virtualised environment. The conceptual software architecture is explained, and reasons for design choices, especially regarding the scheduling of concurrent requests, are given. The implementation of the application's main components and their interactions are described in-depth. The API of the REST server is documented, and a brief guide on configuration and set-up of the server is given. The performance of the software, especially in a concurrent setting, is discussed. Different factors that have an effect on the performance, like the use of a RAM drive, are analyzed. Finally, there is some discussion of extensibility of the software to accommodate additional use cases.